Kubus

equivlib/equiv.ktt

Contractible types, fibers, equivalences, univalence as a map ua, isomorphisms are equivalences.

13 declarations, all certified by the kernel · source

1import basic
2
3✓def isContr (A : U) : U := (x : A) × ((y : A) -> Path A x y)
4✓def fiber {A B : U} (f : A -> B) (y : B) : U := (x : A) × Path B (f x) y
5✓def isEquiv {A B : U} (f : A -> B) : U := (y : B) -> isContr (fiber f y)
6✓def Equiv (A B : U) : U := (f : A -> B) × isEquiv f
7
8✓def idIsEquiv {A : U} : isEquiv (id {A}) :=
9 \y -> ((y, refl y), \z i -> (z.2 (~i), \j -> z.2 (~i \/ j)))
11✓def idEquiv (A : U) : Equiv A A := (id, idIsEquiv)
13✓def ua {A B : U} (e : Equiv A B) : Path U A B :=
14 \i -> Glue B [i = 0 -> (A, e), i = 1 -> (B, idEquiv B)]
16-- transport along ua is e.1, up to a path: unglue the filler of the transport
17✓def uaβ {A B : U} (e : Equiv A B) (x : A) : Path B (e.1 x) (transport (ua e) x) :=
18 \i -> unglue (fill j (ua e j) [] x i)
20-- isomorphisms are equivalences
21✓def section {A B : U} (f : A -> B) (g : B -> A) : U := (b : B) -> Path B (f (g b)) b
22✓def retract {A B : U} (f : A -> B) (g : B -> A) : U := (a : A) -> Path A (g (f a)) a
24✓def lemIso {A B : U} {f : A -> B} {g : B -> A} (s : section f g) (t : retract f g)
25 {y : B} {x0 x1 : A} (p0 : Path B (f x0) y) (p1 : Path B (f x1) y)
26 : Path (fiber f y) (x0, p0) (x1, p1) :=
27 let fill0 : (i : I) -> (k : I) -> A :=
28 \i k -> fill k A [i = 1 -> t x0 k, i = 0 -> g y] (g (p0 (~i))) k in
29 let fill1 : (i : I) -> (k : I) -> A :=
30 \i k -> fill k A [i = 1 -> t x1 k, i = 0 -> g y] (g (p1 (~i))) k in
31 let fill2 : (i : I) -> (k : I) -> A :=
32 \i k -> fill k A [i = 1 -> fill1 k 1, i = 0 -> fill0 k 1] (g y) k in
33 let p : Path A x0 x1 := \i -> fill2 i 1 in
34 let sq : (i : I) -> (j : I) -> A :=
35 \i j -> hcomp k A [i = 1 -> fill1 j (~k), i = 0 -> fill0 j (~k),
36 j = 1 -> t (fill2 i 1) (~k), j = 0 -> g y] (fill2 i j) in
37 let sq1 : (i : I) -> (j : I) -> B :=
38 \i j -> hcomp k B [i = 1 -> s (p1 (~j)) k, i = 0 -> s (p0 (~j)) k,
39 j = 1 -> s (f (p i)) k, j = 0 -> s y k] (f (sq i j)) in
40 \i -> (p i, \j -> sq1 i (~j))
42✓def isoToEquiv {A B : U} (f : A -> B) (g : B -> A) (s : section f g) (t : retract f g) : Equiv A B :=
43 (f, \y -> ((g y, s y), \z -> lemIso s t (s y) z.2))
45✓def isoToPath {A B : U} (f : A -> B) (g : B -> A) (s : section f g) (t : retract f g) : Path U A B :=
46 ua (isoToEquiv f g s t)