Kubus

univalencelib/univalence.ktt

The univalence axiom: the type of types equivalent to A is contractible.

6 declarations, all certified by the kernel · source

1import equiv
2
3-- Univalence, in the form: the type of types equivalent to A is contractible.
4-- The proof glues A along the given equivalence; unglue is an equivalence.
5
6✓def equivCtr {A B : U} (e : Equiv A B) (y : B) : fiber e.1 y := (e.2 y).1
7
8✓def equivCtrPath {A B : U} (e : Equiv A B) (y : B) (v : fiber e.1 y)
9 : Path (fiber e.1 y) (equivCtr e y) v := (e.2 y).2 v
11✓def GlueI {A : U} (w : (T : U) × Equiv T A) (i : I) : U :=
12 Glue A [i = 0 -> (A, idEquiv A), i = 1 -> w]
14✓def unglueI {A : U} (w : (T : U) × Equiv T A) (i : I) (g : GlueI w i) : A := unglue g
16✓def unglueIsEquivI {A : U} (w : (T : U) × Equiv T A) (i : I) : isEquiv (unglueI w i) :=
17 \b ->
18 let c0 : fiber (idEquiv A).1 b := equivCtr (idEquiv A) b in
19 let c1 : fiber w.2.1 b := equivCtr w.2 b in
20 let ctr : fiber (unglueI w i) b :=
21 (glue [i = 0 -> c0.1, i = 1 -> c1.1] (hcomp j A [i = 0 -> c0.2 (~j), i = 1 -> c1.2 (~j)] b),
22 \j -> hfill k A [i = 0 -> c0.2 (~k), i = 1 -> c1.2 (~k)] b (~j)) in
23 (ctr, \v l ->
24 (glue [i = 0 -> (equivCtrPath (idEquiv A) b v l).1, i = 1 -> (equivCtrPath w.2 b v l).1]
25 (hcomp j A [i = 0 -> (equivCtrPath (idEquiv A) b v l).2 (~j),
26 i = 1 -> (equivCtrPath w.2 b v l).2 (~j),
27 l = 0 -> hfill k A [i = 0 -> c0.2 (~k), i = 1 -> c1.2 (~k)] b j,
28 l = 1 -> v.2 (~j)] b),
29 \j -> hfill k A [i = 0 -> (equivCtrPath (idEquiv A) b v l).2 (~k),
30 i = 1 -> (equivCtrPath w.2 b v l).2 (~k),
31 l = 0 -> hfill m A [i = 0 -> c0.2 (~m), i = 1 -> c1.2 (~m)] b k,
32 l = 1 -> v.2 (~k)] b (~j)))
34✓def EquivContr (A : U) : isContr^1 ((T : U) × Equiv T A) :=
35 ((A, idEquiv A), \w i -> (GlueI w i, (unglueI w i, unglueIsEquivI w i)))