David Corfield


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

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

a,b:A,f:[A,B],p:Id A(a,b)f*(p):Id B(f(a),f(b))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= Ay)(f(x)= Bf(y))ap_f: (x =_A y)\to (f(x) =_B f(y)).

Presumably by path induction, map sends refl A(a)refl_A(a) to refl B(f(a))refl_B(f(a)).


x,y:A,p:Id A(x,y)C(x,y,p):= (B,f): X:Type[A,X]Id B(f(x),f(y)):Typex, 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))d(x): C(x,x,refl_A(x)) where d(x)(B,f)=refl B(f(x))d(x)(B,f) = refl_B(f(x)) generates a general c(x,y,p)c(x, y, p) with c(x,x,refl A(x))=d(x)c(x, x, refl_A(x)) = d(x).

What if BB is 𝒰\mathcal{U}? So that ff is a dependent type.

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

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

Or maps into XX, such as homotopy, π n\pi_n, which are groups for i>0i \gt 0.


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

Alibi(c,e)=¬(Id(placep(c,t(e)),placev(e)) Alibi(c,e) = \neg(Id(placep(c, t(e)), placev(e))
¬(Id(c,a(e))\neg(Id(c, a(e))
placep(a(e),t(e))=placev(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.