The Fundamental Theorem of Identity Types
Table of Contents
1 Fundamental Theorem of Identity
module Lib.FundamentalTheorem where
This file shows Rijke's fundamental theorem of identity types (§11 of his introduction to homotopy type theory).
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.QInv import Lib.Data.Nat import Lib.Prop.BiInv import Lib.Prop.Comp import Lib.Prop.Equiv import Lib.Prop.Paths
1.2 Families of equivalences
We define maps of total spaces.
tot (A : U) (B C : A → U) (f : (x : A) → B x → C x) : Σ A B → Σ A C = λxy. (xy.1, f xy.1 xy.2)
1.2.1 Equivalence between fibrations of tot
There is an equivalence between the fibrations of tot f and f (pr1 t).
tot/fib-equiv-map/refl (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (y : B x) : Fib (B x) (C x) (f x) (f x y) = (y, refl (C x) (f x y)) tot/fib-equiv-map/sg (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (z : C x) (t : Σ A B) (p : Path (Σ A C) (tot A B C f t) (x, z)) : Fib (B x) (C x) (f x) z = J ( Σ A C) ( tot A B C f t) ( λu _. Fib (B u.1) (C u.1) (f u.1) u.2) ( tot/fib-equiv-map/refl A B C f t.1 t.2) ( x, z) p tot/fib-equiv-map (A : U) (B C : A → U) (f : (x : A) → B x → C x) (t : Σ A C) : (Fib (Σ A B) (Σ A C) (tot A B C f) t) → Fib (B t.1) (C t.1) (f t.1) t.2 = λu. tot/fib-equiv-map/sg A B C f t.1 t.2 u.1 (inv (Σ A C) t (tot A B C f u.1) u.2)
Indeed, the previous function has an inverse.
tot/fib-equiv-inv-map/refl (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (y : B x) : Fib (Σ A B) (Σ A C) (tot A B C f) (x, (f x y)) = ((x, y), refl (Σ A C) (x, f x y)) tot/fib-equiv-inv-map/sg (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (z : C x) (y : B x) (p : Path (C x) (f x y) z) : Fib (Σ A B) (Σ A C) (tot A B C f) (x, z) = J (C x) (f x y) (λc _. Fib (Σ A B) (Σ A C) (tot A B C f) (x, c)) (tot/fib-equiv-inv-map/refl A B C f x y) z p tot/fib-equiv-inv-map (A : U) (B C : A → U) (f : (x : A) → B x → C x) (t : Σ A C) : (Fib (B t.1) (C t.1) (f t.1) t.2) → Fib (Σ A B) (Σ A C) (tot A B C f) t = λu. tot/fib-equiv-inv-map/sg A B C f t.1 t.2 u.1 (inv (C t.1) t.2 (f t.1 u.1) u.2)
By pattern-matching and path induction, we can build the right homotopy. We have to be careful as (i) we inverse the paths in the functions definitions and (ii) as we are in a cubical prover, J is not the computation rule for Path, so we need to use J/comp to conclude the proof.
tot/fib-equiv-right-htpy/refl' (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (y : B x) : Path (Fib (B x) (C x) (f x) (f x y)) ((tot/fib-equiv-map A B C f (x, (f x y))) (tot/fib-equiv-inv-map A B C f (x, (f x y)) (y, (refl (C x) (f x y))))) (y, (refl (C x) (f x y))) = let t : Fib (Σ A B) (Σ A C) (tot A B C f) (x, f x y) = tot/fib-equiv-inv-map A B C f (x, (f x y)) (y, (refl (C x) (f x y))) u : Fib (Σ A B) (Σ A C) (tot A B C f) (x, f x y) = tot/fib-equiv-inv-map/sg A B C f x (f x y) y (refl (C x) (f x y)) g : Fib (Σ A B) (Σ A C) (tot A B C f) (x, f x y) → Fib (B x) (C x) (f x) (f x y) = tot/fib-equiv-map A B C f (x, (f x y)) v : Fib (Σ A B) (Σ A C) (tot A B C f) (x, f x y) = ((x, y), refl (Σ A C) (x, f x y)) p : Path (Fib (Σ A B) (Σ A C) (tot A B C f) (x, f x y)) u v = J/comp (C x) (f x y) (λc _. Fib (Σ A B) (Σ A C) (tot A B C f) (x, c)) v in comp-n (Fib (B x) (C x) (f x) (f x y)) four-Nat (g t) (g u) (ap (Path (C x) (f x y) (f x y)) (Fib (B x) (C x) (f x) (f x y)) (λq. g (tot/fib-equiv-inv-map/sg A B C f x (f x y) y q)) (inv (C x) (f x y) (f x y) (refl (C x) (f x y))) (refl (C x) (f x y)) (inv/refl (C x) (f x y))) (g v) (ap (Fib (Σ A B) (Σ A C) (tot A B C f) (x, f x y)) (Fib (B x) (C x) (f x) (f x y)) g u v p) (tot/fib-equiv-map/sg A B C f x (f x y) (x, y) (refl (Σ A C) (x, f x y))) (ap (Path (Σ A C) (x, f x y) (x, f x y)) (Fib (B x) (C x) (f x) (f x y)) (tot/fib-equiv-map/sg A B C f x (f x y) (x, y)) (inv (Σ A C) (x, f x y) (x, f x y) (refl (Σ A C) (x, f x y))) (refl (Σ A C) (x, f x y)) (inv/refl (Σ A C) (x, f x y))) (y, refl (C x) (f x y)) (J/comp (Σ A C) (tot A B C f (x, y)) (λw _. Fib (B w.1) (C w.1) (f w.1) w.2) (y, refl (C x) (f x y))) tot/fib-equiv-right-htpy/refl (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (y : B x) : Path (Fib (B x) (C x) (f x) (f x y)) ((tot/fib-equiv-map A B C f (x, (f x y))) (tot/fib-equiv-inv-map A B C f (x, (f x y)) (y, (inv (C x) (f x y) (f x y) (refl (C x) (f x y)))))) (y, (inv (C x) (f x y) (f x y) (refl (C x) (f x y)))) = let g : (Path (C x) (f x y) (f x y)) → Fib (B x) (C x) (f x) (f x y) = λp. ((tot/fib-equiv-map A B C f (x, (f x y))) (tot/fib-equiv-inv-map A B C f (x, (f x y)) (y, p))) in comp-n (Fib (B x) (C x) (f x) (f x y)) three-Nat (g (inv (C x) (f x y) (f x y) (refl (C x) (f x y)))) (g (refl (C x) (f x y))) (ap (Path (C x) (f x y) (f x y)) (Fib (B x) (C x) (f x) (f x y)) g (inv (C x) (f x y) (f x y) (refl (C x) (f x y))) (refl (C x) (f x y)) (inv/refl (C x) (f x y))) (y, refl (C x) (f x y)) (tot/fib-equiv-right-htpy/refl' A B C f x y) (y, (inv (C x) (f x y) (f x y) (refl (C x) (f x y)))) (ap (Path (C x) (f x y) (f x y)) (Fib (B x) (C x) (f x) (f x y)) (λp. (y, p)) (refl (C x) (f x y)) (inv (C x) (f x y) (f x y) (refl (C x) (f x y))) (inv (Path (C x) (f x y) (f x y)) (inv (C x) (f x y) (f x y) (refl (C x) (f x y))) (refl (C x) (f x y)) (inv/refl (C x) (f x y)))) tot/fib-equiv-right-htpy/sg (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (z : C x) (y : B x) (p : Path (C x) (f x y) z) : Path (Fib (B x) (C x) (f x) z) ((tot/fib-equiv-map A B C f (x, z)) (tot/fib-equiv-inv-map A B C f (x, z) (y, (inv (C x) (f x y) z p)))) (y, (inv (C x) (f x y) z p)) = J (C x) (f x y) (λc q. Path (Fib (B x) (C x) (f x) c) ((tot/fib-equiv-map A B C f (x, c)) (tot/fib-equiv-inv-map A B C f (x, c) (y, (inv (C x) (f x y) c q)))) (y, (inv (C x) (f x y) c q))) (tot/fib-equiv-right-htpy/refl A B C f x y) z p tot/fib-equiv-right-htpy (A : U) (B C : A → U) (f : (x : A) → B x → C x) (t : Σ A C) (u : Fib (B t.1) (C t.1) (f t.1) t.2) : Path (Fib (B t.1) (C t.1) (f t.1) t.2) ((tot/fib-equiv-map A B C f t) (tot/fib-equiv-inv-map A B C f t u)) u = let x : A = t.1 y : B x = u.1 z : C x = t.2 p : Path (C x) z (f x y) = u.2 g : (Path (C x) z (f x y)) → Fib (B x) (C x) (f x) z = λq. (tot/fib-equiv-map A B C f (x, z)) (tot/fib-equiv-inv-map A B C f (x, z) (y, q)) in comp-n (Fib (B x) (C x) (f x) z) three-Nat (g p) (g (inv (C x) (f x y) z (inv (C x) z (f x y) p))) (ap (Path (C x) z (f x y)) (Fib (B x) (C x) (f x) z) g p (inv (C x) (f x y) z (inv (C x) z (f x y) p)) (inv/involutive' (C x) z (f x y) p)) (y, (inv (C x) (f x y) z (inv (C x) z (f x y) p))) (tot/fib-equiv-right-htpy/sg A B C f x z y (inv (C x) z (f x y) p)) (y, p) (ap (Path (C x) z (f x y)) (Fib (B x) (C x) (f x) z) (λq. (y, q)) (inv (C x) (f x y) z (inv (C x) z (f x y) p)) p (inv/involutive (C x) z (f x y) p))
We can also build the left homotopy with more or less as much work.
-- J/comp (A : U) (x : A) (M : (y : A) (p : Path A x y) → U) (m : M x (refl A x)) : Path (M x (refl A x)) (J A x M m x (refl A x)) m tot/fib-equiv-left-htpy/refl (A : U) (B C : A → U) (f : (x : A) → B x → C x) (t : Σ A B) : Path (Fib (Σ A B) (Σ A C) (tot A B C f) (tot A B C f t)) ((tot/fib-equiv-inv-map A B C f (tot A B C f t)) (tot/fib-equiv-map A B C f (tot A B C f t) (t, (inv (Σ A C) (tot A B C f t) (tot A B C f t) (refl (Σ A C) (tot A B C f t)))))) (t, inv (Σ A C) (tot A B C f t) (tot A B C f t) (refl (Σ A C) (tot A B C f t))) = let u : Σ A C = tot A B C f t T : U = Fib (Σ A B) (Σ A C) (tot A B C f) u v : T = (t, (inv (Σ A C) u u (refl (Σ A C) u))) x : A = t.1 y : B x = t.2 a : T = ((tot/fib-equiv-inv-map A B C f u) (tot/fib-equiv-map A B C f u (t, refl (Σ A C) u))) b : T = ((tot/fib-equiv-inv-map A B C f u) (tot/fib-equiv-map/sg A B C f u.1 u.2 t (refl (Σ A C) u))) c : T = tot/fib-equiv-inv-map A B C f u (y, refl (C x) (f x y)) d : T = tot/fib-equiv-inv-map/sg A B C f u.1 u.2 y (refl (C x) (f x y)) e : T = ((x, y), refl (Σ A C) (x, f x y)) in comp-n T six-Nat ((tot/fib-equiv-inv-map A B C f u) (tot/fib-equiv-map A B C f u (t, inv (Σ A C) u u (refl (Σ A C) u)))) a (ap (Path (Σ A C) u u) T (λp. ((tot/fib-equiv-inv-map A B C f u) (tot/fib-equiv-map A B C f u (t, p)))) (inv (Σ A C) u u (refl (Σ A C) u)) (refl (Σ A C) u) (inv/refl (Σ A C) u)) b (ap (Path (Σ A C) u u) T (λp. ((tot/fib-equiv-inv-map A B C f u) (tot/fib-equiv-map/sg A B C f u.1 u.2 t p))) (inv (Σ A C) u u (refl (Σ A C) u)) (refl (Σ A C) u) (inv/refl (Σ A C) u)) c (ap (Fib (B x) (C x) (f x) u.2) T (λp. tot/fib-equiv-inv-map A B C f u p) (tot/fib-equiv-map/sg A B C f u.1 u.2 t (refl (Σ A C) u)) (y, refl (C x) (f x y)) (J/comp (Σ A C) u (λu' _. Fib (B u'.1) (C u'.1) (f u'.1) u'.2) (y, refl (C x) (f x y)))) d (ap (Path (C x) (f x y) (f x y)) T (λp. tot/fib-equiv-inv-map/sg A B C f u.1 u.2 y p) (inv (C x) (f x y) (f x y) (refl (C x) (f x y))) (refl (C x) (f x y)) (inv/refl (C x) (f x y))) e (J/comp (C x) (f x y) (λc' _. Fib (Σ A B) (Σ A C) (tot A B C f) (x, c')) ((x, y), refl (Σ A C) (x, f x y))) ((x, y), inv (Σ A C) (x, f x y) (x, f x y) (refl (Σ A C) (x, f x y))) (ap (Path (Σ A C) (x, f x y) (x, f x y)) T (λp. ((x, y), p)) (refl (Σ A C) (x, f x y)) (inv (Σ A C) (x, f x y) (x, f x y) (refl (Σ A C) (x, f x y))) (refl/sym (Σ A C) (x, f x y))) tot/fib-equiv-left-htpy/sg (A : U) (B C : A → U) (f : (x : A) → B x → C x) (x : A) (z : C x) (t : Σ A B) (p : Path (Σ A C) (tot A B C f t) (x, z)) : Path (Fib (Σ A B) (Σ A C) (tot A B C f) (x, z)) ((tot/fib-equiv-inv-map A B C f (x, z)) (tot/fib-equiv-map A B C f (x, z) (t, (inv (Σ A C) (tot A B C f t) (x, z) p)))) (t, inv (Σ A C) (tot A B C f t) (x, z) p) = J (Σ A C) (tot A B C f t) (λu q. Path (Fib (Σ A B) (Σ A C) (tot A B C f) u) ((tot/fib-equiv-inv-map A B C f u) (tot/fib-equiv-map A B C f u (t, (inv (Σ A C) (tot A B C f t) u q)))) (t, inv (Σ A C) (tot A B C f t) u q)) (tot/fib-equiv-left-htpy/refl A B C f t) (x, z) p tot/fib-equiv-left-htpy (A : U) (B C : A → U) (f : (x : A) → B x → C x) (t : Σ A C) (u : Fib (Σ A B) (Σ A C) (tot A B C f) t) : Path (Fib (Σ A B) (Σ A C) (tot A B C f) t) ((tot/fib-equiv-inv-map A B C f t) (tot/fib-equiv-map A B C f t u)) u = comp-n (Fib (Σ A B) (Σ A C) (tot A B C f) t) three-Nat ((tot/fib-equiv-inv-map A B C f t) (tot/fib-equiv-map A B C f t u)) ((tot/fib-equiv-inv-map A B C f t) (tot/fib-equiv-map A B C f t (u.1, inv (Σ A C) (tot A B C f u.1) t (inv (Σ A C) t (tot A B C f u.1) u.2)))) (ap (Path (Σ A C) t (tot A B C f u.1)) (Fib (Σ A B) (Σ A C) (tot A B C f) t) (λp. (tot/fib-equiv-inv-map A B C f t) (tot/fib-equiv-map A B C f t (u.1, p))) u.2 (inv (Σ A C) (tot A B C f u.1) t (inv (Σ A C) t (tot A B C f u.1) u.2)) (inv/involutive' (Σ A C) t (tot A B C f u.1) u.2)) (u.1, inv (Σ A C) (tot A B C f u.1) t (inv (Σ A C) t (tot A B C f u.1) u.2)) (tot/fib-equiv-left-htpy/sg A B C f t.1 t.2 u.1 (inv (Σ A C) t (tot A B C f u.1) u.2)) u (ap (Path (Σ A C) t (tot A B C f u.1)) (Fib (Σ A B) (Σ A C) (tot A B C f) t) (λp. (u.1, p)) (inv (Σ A C) (tot A B C f u.1) t (inv (Σ A C) t (tot A B C f u.1) u.2)) u.2 (inv/involutive (Σ A C) t (tot A B C f u.1) u.2))
Thus, Fib tot f t is equivalent to Fib (f(pr1 t)) (pr2 t).
tot/Equiv-fib (A : U) (B C : A → U) (f : (x : A) → B x → C x) (t : Σ A C) : Equiv (Fib (Σ A B) (Σ A C) (tot A B C f) t) (Fib (B t.1) (C t.1) (f t.1) t.2) = has-inverse/Equiv (Fib (Σ A B) (Σ A C) (tot A B C f) t) (Fib (B t.1) (C t.1) (f t.1) t.2) (tot/fib-equiv-map A B C f t) (tot/fib-equiv-inv-map A B C f t, (tot/fib-equiv-right-htpy A B C f t, tot/fib-equiv-left-htpy A B C f t))
1.2.2 Equivalence between maps
If f is as before, then f is a family of equivalences iff tot f is an equivalence.
fam-equiv/is-equiv-tot (A : U) (B C : A → U) (f : (x : A) → B x → C x) (e : (x : A) → is-equiv (B x) (C x) (f x)) : is-equiv (Σ A B) (Σ A C) (tot A B C f) = is-equiv/Sg-fam A B C (λx. (f x, e x)) fam-equiv/Equiv-tot (A : U) (B C : A → U) (f : (x : A) → B x → C x) (e : (x : A) → is-equiv (B x) (C x) (f x)) : Equiv (Σ A B) (Σ A C) = Equiv/Sg-fam A B C (λx. (f x, e x)) is-equiv-tot/fam-equiv (A : U) (B C : A → U) (f : (x : A) → B x → C x) (e : is-equiv (Σ A B) (Σ A C) (tot A B C f)) (x : A) : is-equiv (B x) (C x) (f x) = λz. is-contr/is-contr-equiv' ( Fib (Σ A B) (Σ A C) (tot A B C f) (x, z)) ( Fib (B x) (C x) (f x) z) ( tot/Equiv-fib A B C f (x, z)) (e (x, z))
1.3 Σ-equivalences
We show that if f : A → B is an equivalence, then the map Σ (x : A) (C (f x)) → Σ B C is an equivalence.
Sg/equiv-base-map (A B : U) (C : B → U) (f : A → B) : Σ A (λx. C (f x)) → Σ B C = λu. let x : A = u.1 z : C (f x) = u.2 in (f x, z)
1.3.1 Bi-invertible map between fibrations
There is a bi-invertible map between the fibrations of equiv-base-map t and f (pr1 t).
Sg/equiv-base-fib-map/refl (A B : U) (C : B → U) (f : A → B) (x : A) (z : C (f x)) : (Fib A B f (f x)) = (x, refl B (f x)) Sg/equiv-base-fib-map/sg (A B : U) (C : B → U) (f : A → B) (y : B) (z' : C y) (x : A) (z : C (f x)) (p : Path (Σ B C) (y, z') (f x, z)) : (Fib A B f y) = J (Σ B C) (f x, z) (λu _. Fib A B f u.1) (Sg/equiv-base-fib-map/refl A B C f x z) (y, z') (inv (Σ B C) (y, z') (f x, z) p) Sg/equiv-base-fib-map (A B : U) (C : B → U) (f : A → B) (t : Σ B C) : (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t) → (Fib A B f t.1) = λu. Sg/equiv-base-fib-map/sg A B C f t.1 t.2 u.1.1 u.1.2 u.2
We can define the inverse map the same way.
Sg/equiv-base-fib-inv-map/refl (A B : U) (C : B → U) (f : A → B) (x : A) (z : C (f x)) : (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) ((f x), z)) = ((x, z), refl (Σ B C) (f x, z)) Sg/equiv-base-fib-inv-map/sg (A B : U) (C : B → U) (f : A → B) (y : B) (z : C y) (x : A) (p : Path B y (f x)) : (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y, z)) = J B (f x) (λy' _. (z' : C y') → (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y', z'))) (λz'. Sg/equiv-base-fib-inv-map/refl A B C f x z') y (inv B y (f x) p) z Sg/equiv-base-fib-inv-map (A B : U) (C : B → U) (f : A → B) (t : Σ B C) : (Fib A B f t.1) → (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t) = λu. Sg/equiv-base-fib-inv-map/sg A B C f t.1 t.2 u.1 u.2
We need to work for the right homotopy, for the same reasons as before.
Sg/equiv-base-fib-right-htpy/refl (A B : U) (C : B → U) (f : A → B) (x : A) (z : C (f x)) : Path (Fib A B f (f x)) ((Sg/equiv-base-fib-map A B C f (f x, z)) (Sg/equiv-base-fib-inv-map A B C f (f x, z) (x, inv B (f x) (f x) (refl B (f x))))) (x, inv B (f x) (f x) (refl B (f x))) = let phi : Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (f x, z) → Fib A B f (f x) = Sg/equiv-base-fib-map A B C f (f x, z) h : (Path B (f x) (f x)) → Fib A B f (f x) = λp. phi (J B (f x) (λy' _. (z' : C y') → (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y', z'))) (λz'. Sg/equiv-base-fib-inv-map/refl A B C f x z') (f x) p z) k : (Path (Σ B C) (f x, z) (f x, z)) → (Fib A B f (f x)) = λp. J (Σ B C) (f x, z) (λu _. Fib A B f u.1) (Sg/equiv-base-fib-map/refl A B C f x z) (f x, z) p a : Fib A B f (f x) = h (refl B (f x)) b : Fib A B f (f x) = phi ((x, z), refl (Σ B C) (f x, z)) c : Fib A B f (f x) = k (refl (Σ B C) (f x, z)) in comp-n (Fib A B f (f x)) six-Nat (phi (Sg/equiv-base-fib-inv-map A B C f (f x, z) (x, inv B (f x) (f x) (refl B (f x))))) (phi (Sg/equiv-base-fib-inv-map A B C f (f x, z) (x, (refl B (f x))))) (ap (Path B (f x) (f x)) (Fib A B f (f x)) (λq. phi (Sg/equiv-base-fib-inv-map A B C f (f x, z) (x, q))) (inv B (f x) (f x) (refl B (f x))) (refl B (f x)) (inv/refl B (f x))) a (ap (Path B (f x) (f x)) (Fib A B f (f x)) h (inv B (f x) (f x) (refl B (f x))) (refl B (f x)) (inv/refl B (f x))) b (ap (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (f x, z)) (Fib A B f (f x)) (λu. phi u) (J B (f x) (λy' _. (z' : C y') → (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y', z'))) (λz'. Sg/equiv-base-fib-inv-map/refl A B C f x z') (f x) (refl B (f x)) z) ((x, z), refl (Σ B C) (f x, z)) (λi. (J/comp B (f x) (λy' _. (z' : C y') → (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y', z'))) (λz'. ((x, z'), refl (Σ B C) (f x, z')))) i z)) c (ap (Path (Σ B C) (f x, z) (f x, z)) (Fib A B f (f x)) k (inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z))) (refl (Σ B C) (f x, z)) (inv/refl (Σ B C) (f x, z))) (x, refl B (f x)) (J/comp (Σ B C) (f x, z) (λu _. Fib A B f u.1) (x, refl B (f x))) (x, inv B (f x) (f x) (refl B (f x))) (ap (Path B (f x) (f x)) (Fib A B f (f x)) (λq. (x, q)) (refl B (f x)) (inv B (f x) (f x) (refl B (f x))) (refl/sym B (f x))) Sg/equiv-base-fib-right-htpy/sg' (A B : U) (C : B → U) (f : A → B) (y : B) (z : C y) (x : A) (p : Path B (f x) y) : Path (Fib A B f y) ((Sg/equiv-base-fib-map A B C f (y, z)) (Sg/equiv-base-fib-inv-map A B C f (y, z) (x, (inv B (f x) y p)))) (x, (inv B (f x) y p)) = J B (f x) (λy' q. (z' : C y') → Path (Fib A B f y') ((Sg/equiv-base-fib-map A B C f (y', z')) (Sg/equiv-base-fib-inv-map A B C f (y', z') (x, (inv B (f x) y' q)))) (x, (inv B (f x) y' q))) (λz'. Sg/equiv-base-fib-right-htpy/refl A B C f x z') y p z Sg/equiv-base-fib-right-htpy/sg (A B : U) (C : B → U) (f : A → B) (y : B) (z : C y) (x : A) (p : Path B y (f x)) : Path (Fib A B f y) ((Sg/equiv-base-fib-map A B C f (y, z)) (Sg/equiv-base-fib-inv-map A B C f (y, z) (x, p))) (x, p) = comp-n (Fib A B f y) three-Nat ((Sg/equiv-base-fib-map A B C f (y, z)) (Sg/equiv-base-fib-inv-map A B C f (y, z) (x, p))) ((Sg/equiv-base-fib-map A B C f (y, z)) (Sg/equiv-base-fib-inv-map A B C f (y, z) (x, (inv B (f x) y (inv B y (f x) p))))) (ap (Path B y (f x)) (Fib A B f y) (λq. (Sg/equiv-base-fib-map A B C f (y, z)) (Sg/equiv-base-fib-inv-map A B C f (y, z) (x, q))) p (inv B (f x) y (inv B y (f x) p)) (inv/involutive' B y (f x) p)) (x, inv B (f x) y (inv B y (f x) p)) (Sg/equiv-base-fib-right-htpy/sg' A B C f y z x (inv B y (f x) p)) (x, p) (ap (Path B y (f x)) (Fib A B f y) (λq. (x, q)) (inv B (f x) y (inv B y (f x) p)) p (inv/involutive B y (f x) p)) Sg/equiv-base-fib-right-htpy (A B : U) (C : B → U) (f : A → B) (t : Σ B C) : Htpy' (Fib A B f t.1) (Fib A B f t.1) (λx. (Sg/equiv-base-fib-map A B C f t) (Sg/equiv-base-fib-inv-map A B C f t x)) (id (Fib A B f t.1)) = λu. Sg/equiv-base-fib-right-htpy/sg A B C f t.1 t.2 u.1 u.2
And we need to work as much for the left homotopy.
Sg/equiv-base-fib-left-htpy/refl (A B : U) (C : B → U) (f : A → B) (x : A) (z : C (f x)) : Path (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (f x, z)) ((Sg/equiv-base-fib-inv-map A B C f (f x, z)) (Sg/equiv-base-fib-map A B C f (f x, z) ((x, z), (inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z)))))) ((x, z), (inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z)))) = let T : (Σ B C) → U = λt. Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) t phi : T (f x, z) → Fib A B f (f x) = Sg/equiv-base-fib-map A B C f (f x, z) psi : Fib A B f (f x) → T (f x, z) = Sg/equiv-base-fib-inv-map A B C f (f x, z) h : (Path (Σ B C) (f x, z) (f x, z)) → T (f x, z) = λp. psi (J (Σ B C) (f x, z) (λu _. Fib A B f u.1) (Sg/equiv-base-fib-map/refl A B C f x z) (f x, z) p) k : (Path B (f x) (f x)) → T (f x, z) = λp. J B (f x) (λy' _. (z' : C y') → T (y', z')) (λz'. Sg/equiv-base-fib-inv-map/refl A B C f x z') (f x) p z a : T (f x, z) = psi (phi ((x, z), refl (Σ B C) (f x, z))) b : T (f x, z) = h (refl (Σ B C) (f x, z)) c : T (f x, z) = psi (x, refl B (f x)) d : T (f x, z) = k (refl B (f x)) in comp-n (T (f x, z)) six-Nat (psi (phi ((x, z), inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z))))) a (ap (Path (Σ B C) (f x, z) (f x, z)) (T (f x, z)) (λq. psi (phi ((x, z), q))) (inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z))) (refl (Σ B C) (f x, z)) (inv/refl (Σ B C) (f x, z))) b (ap (Path (Σ B C) (f x, z) (f x, z)) (T (f x, z)) h (inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z))) (refl (Σ B C) (f x, z)) (inv/refl (Σ B C) (f x, z))) c (ap (Fib A B f (f x)) (T (f x, z)) psi (J (Σ B C) (f x, z) (λu _. Fib A B f u.1) (Sg/equiv-base-fib-map/refl A B C f x z) (f x, z) (refl (Σ B C) (f x, z))) (x, refl B (f x)) (J/comp (Σ B C) (f x, z) (λu _. Fib A B f u.1) (x, refl B (f x)))) d (ap (Path B (f x) (f x)) (T (f x, z)) k (inv B (f x) (f x) (refl B (f x))) (refl B (f x)) (inv/refl B (f x))) ((x, z), refl (Σ B C) (f x, z)) (λi. (J/comp B (f x) (λy' _. (z' : C y') → (T (y', z'))) (λz'. ((x, z'), refl (Σ B C) (f x, z')))) i z) ((x, z), inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z))) (ap (Path (Σ B C) (f x, z) (f x, z)) (T (f x, z)) (λq. ((x, z), q)) (refl (Σ B C) (f x, z)) (inv (Σ B C) (f x, z) (f x, z) (refl (Σ B C) (f x, z))) (refl/sym (Σ B C) (f x, z))) Sg/equiv-base-fib-left-htpy/sg' (A B : U) (C : B → U) (f : A → B) (y : B) (z' : C y) (x : A) (z : C (f x)) (p : Path (Σ B C) (f x, z) (y, z')) : Path (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y, z')) ((Sg/equiv-base-fib-inv-map A B C f (y, z')) (Sg/equiv-base-fib-map A B C f (y, z') ((x, z), (inv (Σ B C) (f x, z) (y, z') p)))) ((x, z), (inv (Σ B C) (f x, z) (y, z') p)) = J (Σ B C) (f x, z) (λt q. Path (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) t) ((Sg/equiv-base-fib-inv-map A B C f t) (Sg/equiv-base-fib-map A B C f t ((x, z), (inv (Σ B C) (f x, z) t q)))) ((x, z), (inv (Σ B C) (f x, z) t q))) (Sg/equiv-base-fib-left-htpy/refl A B C f x z) (y, z') p Sg/equiv-base-fib-left-htpy/sg (A B : U) (C : B → U) (f : A → B) (y : B) (z' : C y) (x : A) (z : C (f x)) (p : Path (Σ B C) (y, z') (f x, z)) : Path (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y, z')) ((Sg/equiv-base-fib-inv-map A B C f (y, z')) (Sg/equiv-base-fib-map A B C f (y, z') ((x, z), p))) ((x, z), p) = comp-n (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y, z')) three-Nat ((Sg/equiv-base-fib-inv-map A B C f (y, z')) (Sg/equiv-base-fib-map A B C f (y, z') ((x, z), p))) ((Sg/equiv-base-fib-inv-map A B C f (y, z')) (Sg/equiv-base-fib-map A B C f (y, z') ((x, z), (inv (Σ B C) (f x, z) (y, z') (inv (Σ B C) (y, z') (f x, z) p))))) (ap (Path (Σ B C) (y, z') (f x, z)) (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y, z')) (λq. (Sg/equiv-base-fib-inv-map A B C f (y, z')) (Sg/equiv-base-fib-map A B C f (y, z') ((x, z), q))) p (inv (Σ B C) (f x, z) (y, z') (inv (Σ B C) (y, z') (f x, z) p)) (inv/involutive' (Σ B C) (y, z') (f x, z) p)) ((x, z), inv (Σ B C) (f x, z) (y, z') (inv (Σ B C) (y, z') (f x, z) p)) (Sg/equiv-base-fib-left-htpy/sg' A B C f y z' x z (inv (Σ B C) (y, z') (f x, z) p)) ((x, z), p) (ap (Path (Σ B C) (y, z') (f x, z)) (Fib (Σ A (λx'. C (f x'))) (Σ B C) (Sg/equiv-base-map A B C f) (y, z')) (λq. ((x, z), q)) (inv (Σ B C) (f x, z) (y, z') (inv (Σ B C) (y, z') (f x, z) p)) p (inv/involutive (Σ B C) (y, z') (f x, z) p)) Sg/equiv-base-fib-left-htpy (A B : U) (C : B → U) (f : A → B) (t : Σ B C) : Htpy' (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t) (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t) (λx. (Sg/equiv-base-fib-inv-map A B C f t) (Sg/equiv-base-fib-map A B C f t x)) (id (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t)) = λu. Sg/equiv-base-fib-left-htpy/sg A B C f t.1 t.2 u.1.1 u.1.2 u.2
Thus, the fibrations of equiv-base-map are bi-invertible.
Sg/equiv-base-is-bi-inv (A B : U) (C : B → U) (f : A → B) (t : Σ B C) : is-bi-inv (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t) (Fib A B f t.1) (Sg/equiv-base-fib-map A B C f t) = has-inverse-is-bi-inv (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t) (Fib A B f t.1) (Sg/equiv-base-fib-map A B C f t) (Sg/equiv-base-fib-inv-map A B C f t, (Sg/equiv-base-fib-right-htpy A B C f t, Sg/equiv-base-fib-left-htpy A B C f t))
1.3.2 Equivalence
To conlude, equiv-base-map is a contractible map iff f is a contractible map, that is, if f is an equivalence, then equiv-base-map is also an equivalence.
Sg/equiv-base-is-equiv (A B : U) (C : B → U) (f : A → B) (H : is-equiv A B f) : is-equiv (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) = λt. is-bi-inv/is-contr-is-bi-inv (Fib (Σ A (λx. C (f x))) (Σ B C) (Sg/equiv-base-map A B C f) t) (Fib A B f t.1) (Sg/equiv-base-fib-map A B C f t) (Sg/equiv-base-is-bi-inv A B C f t) (H t.1) Sg/equiv-base (A B : U) (C : B → U) (e : Equiv A B) : Equiv (Σ A (λx. C (Equiv/map A B e x))) (Σ B C) = (Sg/equiv-base-map A B C (Equiv/map A B e), Sg/equiv-base-is-equiv A B C (Equiv/map A B e) (Equiv/is-equiv A B e)) Sg/equiv-base' (A B : U) (C : B → U) (e : Equiv A B) : Equiv (Σ B C) (Σ A (λx. C (Equiv/map A B e x))) = Equiv/sym ( Σ A (λx. C (Equiv/map A B e x))) ( Σ B C) ( Sg/equiv-base A B C e)
1.4 The fundamental theorem
We use the previous result to show the fundamental theorem of identity, that is: the family of maps f : (x : A) → (a = x) → B x is a family of equivalences iff the total space (Σ A B) is contractible.
By the theorem fam-equiv/Equiv-tot, if the family of maps f is an equivalence then (Σ (x : A) (a = x)) is equivalent to (Σ A B) and (Σ (x : A) (a = x)) is contractible.
fundamental-theorem-id (A : U) (B : A → U) (a : A) (f : (x : A) → (Path A a x) → B x) (c : is-contr (Σ A B)) (x : A) : is-equiv (Path A a x) (B x) (f x) = is-equiv-tot/fam-equiv A (λy. Path A a y) B f (is-contr/is-equiv (Σ A (λy. Path A a y)) (Σ A B) (tot A (λy. Path A a y) B f) (is-contr/Sg-path-is-contr A a) c) x fundamental-theorem-id' (A : U) (B : A → U) (a : A) (f : (x : A) → (Path A a x) → B x) (e : (x : A) → is-equiv (Path A a x) (B x) (f x)) : is-contr (Σ A B) = is-contr/is-contr-equiv' (Σ A (λx. Path A a x)) (Σ A B) (fam-equiv/Equiv-tot A (λx. Path A a x) B f e) (is-contr/Sg-path-is-contr A a)
1.5 The structure identity principle
This result leads to another result that helps characterize structures. It is easy to show: we use the fact that we can make y and z commute in the types. Then, Σ (Σ A C) ⋅ is contractible as Σ A C is contractible (using Sg/is-contr').
First, let us show that we can make the types commute.
str-principle/map (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) : (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) → (Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) = λt. ((t.1.1, t.2.1), (t.1.2, t.2.2)) str-principle/inv-map (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) : (Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) → (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) = λt. ((t.1.1, t.2.1), (t.1.2, t.2.2)) str-principle/right-htpy/sg (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) (a : A) (b : B a) (c : C a) (d : D a b c) : Path (Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) (str-principle/map A B C D (str-principle/inv-map A B C D ((a, c), (b, d)))) ((a, c), (b, d)) = refl (Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) ((a, c), (b, d)) str-principle/right-htpy (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) (u : Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) : Path (Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) (str-principle/map A B C D (str-principle/inv-map A B C D u)) u = str-principle/right-htpy/sg A B C D u.1.1 u.2.1 u.1.2 u.2.2 str-principle/left-htpy/sg (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) (a : A) (b : B a) (c : C a) (d : D a b c) : Path (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) (str-principle/inv-map A B C D (str-principle/map A B C D ((a, b), (c, d)))) ((a, b), (c, d)) = refl (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) ((a, b), (c, d)) str-principle/left-htpy (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) (u : Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) : Path (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) (str-principle/inv-map A B C D (str-principle/map A B C D u)) u = str-principle/left-htpy/sg A B C D u.1.1 u.1.2 u.2.1 u.2.2 str-principle/is-equiv (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) : is-equiv (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) (Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) (str-principle/map A B C D) = has-inverse/is-equiv ( Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) ( Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) ( str-principle/map A B C D) ( str-principle/inv-map A B C D, ( str-principle/right-htpy A B C D, str-principle/left-htpy A B C D)) str-principle/Equiv (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) : Equiv (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) (Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) = ( str-principle/map A B C D, str-principle/is-equiv A B C D)
Then, we can state the structure identity principle.
str-principle-id (A : U) (B C : A → U) (D : (x : A) → B x → C x → U) (is-contr-AC : is-contr (Σ A C)) (a : A) (c : C a) (is-contr-tot : is-contr (Σ (B a) (λy. D a y c))) : is-contr (Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) = is-contr/is-contr-equiv ( Σ (Σ A B) (λt. Σ (C t.1) (D t.1 t.2))) ( Σ (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2))) ( str-principle/Equiv A B C D) ( Sg/is-contr' (Σ A C) (λt. Σ (B t.1) (λy. D t.1 y t.2)) is-contr-AC (a, c) is-contr-tot)