# 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)$

Last revised on August 29, 2021 at 02:28:04. See the history of this page for a list of all contributions to it.