David Corfield distinguish

Idea

Importance of using maps to distinguish elements of a type. $a, b: A$, then for some $f:[A, B]$, because $\neg Id_{B}(f(a), f(b))$ is true, we know $\neg Id_A(a, b)$. Often choose a $B$ with decidable equality.

We must have a map $Id_A(a, b) \to Id_{B}(f(a), f(b))$ to postcompose with the map to $0$.

$$a, b: A, f:[A, B], p:Id_A(a, b) \vdash f*(p):Id_B(f(a),f(b))$$

Lemma 2.2.1, $ap_f: (x =_A y)\to (f(x) =_B f(y))$.

Presumably by path induction, map sends $refl_A(a)$ to $refl_B(f(a))$.

Or

$$x, y: A, p:Id_A(x, y) \vdash C(x,y,p) := \prod_{(B, f):\sum_{X:Type}[A,X]}Id_{B}(f(x), f(y)): Type$$

Then $d(x): C(x,x,refl_A(x))$ where $d(x)(B,f) = refl_B(f(x))$ generates a general $c(x, y, p)$ with $c(x, x, refl_A(x)) = d(x)$.

What if $B$ is $\mathcal{U}$? So that $f$ is a dependent type.

Then $Id_{\mathcal{U}}(f(a), f(b))$ is equivalent to $Equiv(f(a), f(b))$.

If $A$-cohomology sends $X$ to (truncation of) $[X, A]$, this is a map to $\mathcal{U}$, perhaps equipped with extra structure such as a ring.

Or maps into $X$, such as homotopy, $\pi_n$, which are groups for $i \gt 0$.

Alibi

We have an event $e$, whose agent is $a(e): Person$. Then $placep: \sum_{x:Person} life(x) \to Place$, $placev: Event \to Place$.

$$Alibi(c,e) = \neg(Id(placep(c, t(e)), placev(e))$$

$$\neg(Id(c, a(e))$$

$$placep(a(e), t(e)) = placev(e)$$