hott_chap2.v

Definition id {A} : A -> A := fun x => x.

Arguments id {A} / x.

Definition compose {A B C} :  (B -> C) -> (A -> B) -> (A -> C)
    := fun g f x => g (f x).

Notation "g 'o' f" := (compose g f) (left associativity, at level 37).

Arguments compose {A B C} f g x /.

(** Identity type with the induction principle. *)

Inductive Identity {A} : A -> A -> Type := refl : forall (x : A), Identity x x.

Notation "x == y" := (Identity x y) (at level 70).

(** Lemma 2.1.1 *)

Definition inverse {A} {x y : A} : (x == y) -> (y == x).
Proof.
    intro p.
    induction p.
    apply refl.
Defined.

Notation "! p" := (inverse p) (at level 50).

(** Lemma 2.1.2 *)

Definition concat {A} {x y z : A} : (x == y) -> (y == z) -> (x == z).
Proof.
    intros p q.
    induction p.
    induction q.
    apply refl.
Defined.

Notation "p @ q" := (concat p q) (at level 60).

(** Lemma 2.1.4 *)

Definition left_unit {A} {x y : A} (p : x == y) : refl x @ p == p.
Proof.
    induction p.
    apply refl.
Defined.

Definition right_unit {A} {x y : A} (p : x == y) : p @ refl y == p.
Proof.
    induction p.
    apply refl.
Defined.

Definition left_inverse {A} {x y : A} (p : x == y) : p @ !p == refl x.
Proof.
    induction p.
    apply refl.
Defined.

Definition right_inverse {A} {x y : A} (p : x == y) : !p @ p == refl y.
Proof.
    induction p.
    apply refl.
Defined.

Definition inverse_inverse {A} {x y : A} (p : x == y) : !(!p) == p.
Proof.
    induction p.
    apply refl.
Defined.

Definition assoc {A} {x y z w : A} (p : x == y) (q : y == z) (r : z == w) :
    (p @ q) @ r == p @ (q @ r).
Proof.
    induction p.
    induction q.
    induction r.
    apply refl.
Defined.

(** Horizonal composition and whiskering. *)

Definition concat2 {A} {x y z : A} {p q : x == y} {r s : y == z} (a : p == q) (b : r == s) :
    (p @ r == q @ s).
Proof.
    induction a.
    induction b.
    apply refl.
Defined.

Notation "p @@ q" := (concat2 p q) (at level 61).


Definition whisker_left {A} {x y z : A} (p : x == y) {q r : y == z} (a : q == r) :
    p @ q == p @ r.
Proof.
    exact (refl p @@ a). 
Defined.

Definition whisker_right {A} {x y z : A} {p q : x == y} (a : p == q) (r : y == z) :
    p @ r == q @ r.
Proof.
    exact (a @@ refl r).
Defined.

Definition cancel_left {A} {x y z : A} (p : x == y) (q r : y == z) :
    (p @ q == p @ r) -> (q == r).
Proof.
    intro a.
    induction p.
    exact (!(left_unit _) @ a @ left_unit _).
Defined.

Definition cancel_right {A} {x y z : A} (p q : x == y) (r : y == z) :
    (p @ r == q @ r) -> (p == q).
Proof.
    intro a.
    induction r.
    exact (!(right_unit _) @ a @ right_unit _).
Defined.

Definition whisker_left_left_unit {A} {x y : A} {p q : x == y} (a : p == q) :
    !(left_unit p) @ whisker_left (refl x) a @ left_unit q == a.
Proof.
    induction a as [p].
    induction p.
    simpl.
    apply refl.
Defined.

Definition whisker_right_right_unit {A} {x y : A} {p q : x == y} (a : p == q) :
    !(right_unit p) @ whisker_right a (refl y) @ right_unit q == a.
Proof.
    induction a as [p].
    induction p.
    apply refl.
Defined.

Definition concat_whisker {A} {x y z : A} {p q : x == y} {r s : y == z} (a : p == q) (b : r == s) :
    (whisker_right a r) @ (whisker_left q b) == (whisker_left p b) @ (whisker_right a s).
Proof.
    induction a as [p].
    induction b as [r].
    apply refl.
Defined.

(** Theorem 2.1.6 *)

Definition comm2 {A} {x : A} {a b : refl x == refl x } : a @ b == b @ a.
Proof.
    apply (concat (!(whisker_right_right_unit a @@ whisker_left_left_unit b))).
    apply (concat (right_unit _ @@ right_unit _)). 
    apply (concat (left_unit _ @@ left_unit _)).
    apply (concat (concat_whisker a b)).
    apply (concat (!(left_unit _ @@ left_unit _))).
    apply (concat (!(right_unit _ @@ right_unit _))).
    apply (concat (whisker_left_left_unit b @@ whisker_right_right_unit a)).
    apply refl.
Defined.

(** Lemma 2.2.1 *)

Definition ap {A B} {x y : A} (f : A -> B) : (x == y) -> (f x == f y).
Proof.
    intro p.
    induction p.
    apply refl.
Defined.

(** Lemma 2.2.2 *)

Definition concat_ap {A B} {x y z : A} (f : A -> B) (p : x == y) (q : y == z) :
    ap f (p @ q) == ap f p @ ap f q.
Proof.
    induction p.
    induction q.
    apply refl.
Defined.

Definition inverse_ap {A B} {x y : A} (f : A -> B) (p : x == y) :
    ap f (!p) == !(ap f p).
Proof.
    induction p.
    apply refl.
Defined.

Definition compose_ap {A B C} {x y : A} (f : A -> B) (g : B -> C) (p : x == y) :
    ap g (ap f p) == ap (g o f) p.
Proof.
    induction p.
    apply refl.
Defined.

Definition id_ap {A} {x y : A} (p : x == y) : ap id p == p.
Proof.
    induction p.
    apply refl.
Defined.

(** Lemma 2.3.1 *)

Definition transport {A} {P : A -> Type} {x y : A} (p : x == y) : P x -> P y.
Proof.
    induction p.
    exact id.
Defined.

(** Lemma 2.3.2 *)

Definition lift {A} {P : A -> Type} {x y : A} (u: P x) (p : x == y) :
    existT P x u  == existT P y (transport p u).
Proof.
    induction p.
    apply refl.
Defined.

(** Lemma 2.3.4 *)

Definition apd {A} {P : A -> Type} {x y : A} (f : forall x, P x) (p : x == y) :
    transport p (f x) == f y.
Proof.
    induction p.
    apply refl.
Defined.

(** Lemma 2.3.5 *)

Definition transport_const {A B} {x y : A} (p : x == y) (b : B) :
    transport (P := fun x => B) p b == b.
Proof.
    induction p.
    apply refl.
Defined.

(** Lemma 2.3.8 *)

Definition apd_const {A B} {x y : A} (f : A -> B) (p : x == y) :
    apd f p == transport_const p (f x) @ ap f p.
Proof.
    induction p.
    apply refl.
Defined.

(** Lemma 2.3.9 *)

Definition concat_transport {A} {P : A -> Type} {x y z : A} (p : x == y) (q : y == z) (u : P x) :
    transport q (transport p u) == transport (p @ q) u.
Proof.
    induction p.
    induction q.
    apply refl.
Defined.

(** Lemma 2.3.10 *)

Definition transport_ap {A B} {P : B -> Type} {f : A -> B} {x y : A} (p : x == y) (u : P (f x)) :
    transport (P := P o f) p u == transport (ap f p) u.
Proof.
    induction p.
    apply refl.
Defined.

(** Definition 2.4.1 *)

Definition Homotopy {A} {P : A -> Type} (f g : forall x, P x) := forall x, f x == g x.

Notation "f ~~ g" := (Homotopy f g) (at level 80).

(** Lemma 2.4.2 *)

Definition homotopy_refl {A} {P : A -> Type} (f : forall x, P x) : f ~~ f.
Proof.
    intro x.
    apply refl.
Defined.

Definition homotopy_inverse {A} {P : A -> Type} {f g : forall x, P x} :
    (f ~~ g) -> (g ~~ f).
Proof.
    intros H x.
    exact (inverse (H x)).
Defined.

Definition homotopy_concat {A} {P : A -> Type} {f g h : forall x, P x} :
    (f ~~ g) -> (g ~~ h) -> (f ~~ h).
Proof.
    intros H G x.
    exact (concat (H x) (G x)).
Defined.

(** Lemma 2.4.3 *)

Definition homotopy_natural {A B} {x y : A} (f g : A -> B) (H : f ~~ g) (p : x == y) :
    H x @ ap g p == ap f p @ H y.
Proof.
    induction p.
    exact (right_unit _ @ !(left_unit _)).
Defined.

(** Lemma 2.4.4 *)

Definition endmap_homotopy_commutes {A} {x : A} (f : A -> A) (H : f ~~ id) :
    H (f x) == ap f (H x).
Proof.
    apply cancel_right with (r := H x). 
    exact (!(whisker_left _ (id_ap (H x))) @ (homotopy_natural f id H (H x))).
Defined.

(** Definition 2.4.6 *)

Definition qinv {A B} (f : A -> B) :=
    ({ g : B -> A & (f o g ~~ id) * (g o f ~~ id) })%type.

(** Definition 2.4.10 *)

Definition is_equiv {A B} (f : A -> B) :=
    ({ g : B -> A & f o g ~~ id } * { h : B -> A & h o f ~~ id })%type.

Definition qinv_implies_equiv {A B} {f : A -> B} : qinv f -> is_equiv f. 
Proof.
    intro H.
    destruct H as [g [a b]].
    exact (existT _ g a, existT _ g b).
Defined.

Definition homotopy_whisker_left {A B C} (f : B -> C) {g h : A -> B} (H : g ~~ h) :
    f o g ~~ f o h.
Proof.
    intro x.
    exact (ap f (H x)).
Defined.

Definition homotopy_whisker_right {A B C} {f g : B -> C} (H : f ~~ g) (h : A -> B):
    f o h ~~ g o h.
Proof.
    intro x.
    exact (H (h x)).
Defined.

Definition equiv_implies_qinv {A B} {f : A -> B} : is_equiv f -> qinv f. 
Proof.
    intro H.
    destruct H as [[g a] [h b]].
    exists g.
    split.
    exact a.
    refine (homotopy_concat (homotopy_whisker_right _ f) b).
    exact (homotopy_concat (homotopy_inverse (homotopy_whisker_right b g)) (homotopy_whisker_left h a)).
Defined.

(** Definition 2.4.11 *)

Definition Equiv (A B : Type) := { f : A -> B & is_equiv f }.

Notation "A <~> B" := (Equiv A B) (at level 85).

(** Example 2.4.7 *)

Definition id_equiv {A : Type} : is_equiv (id (A := A)).
Proof.
    apply qinv_implies_equiv.
    exists id.
    split; apply homotopy_refl.
Defined.

(** Lemma 2.4.12 *)

Definition equiv_refl (A : Type) : A <~> A.
Proof.
    exists id.
    apply qinv_implies_equiv.
    exists id.
    split; apply homotopy_refl.
Defined.

Definition equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
Proof.
    intro H.
    destruct H as [f H].
    destruct (equiv_implies_qinv H) as [g [a b]].
    exists g.
    apply qinv_implies_equiv.
    exists f.
    exact (b, a).
Defined.

Definition equiv_concat {A B C : Type} : (A <~> B) -> (B <~> C) -> (A <~> C).
Proof.
    intros H0 H1.
    destruct H0 as [f H0].
    destruct (equiv_implies_qinv H0) as [f' [a b]].
    destruct H1 as [g H1].
    destruct (equiv_implies_qinv H1) as [g' [c d]].
    exists (g o f).
    apply qinv_implies_equiv.
    exists (f' o g').
    split.
    exact (homotopy_concat (homotopy_whisker_right (homotopy_whisker_left g a) g') c).
    exact (homotopy_concat (homotopy_whisker_right (homotopy_whisker_left f' d) f) b).
Defined.

(** Theorem 2.6.2 *)

Definition pair_identity_inv {A B : Type} {x y : A * B} :
    (x == y) -> (fst x == fst y) * (snd x == snd y).
Proof.
    intro p.
    exact (ap (@fst A B) p, ap (@snd A B) p).
Defined.

Definition pair_identity {A B : Type} {x y : A * B} :
    (fst x == fst y) * (snd x == snd y) -> (x == y).
Proof.
    intro H.
    destruct H as [p q].
    destruct x as [a b].
    destruct y as [a' b'].
    simpl in p, q.
    induction p.
    induction q.
    apply refl.
Defined.

Definition pair_identity_equiv {A B : Type} {x y : A * B} :
    (x == y) <~> (fst x == fst y) * (snd x == snd y).
Proof.
    exists pair_identity_inv.
    apply qinv_implies_equiv.
    exists pair_identity.
    split.
    intro pq.
    destruct pq as [p q].
    destruct x as [a b].
    destruct y as [a' b'].
    simpl in p, q.
    induction p.
    induction q.
    apply refl.
    intro r.
    induction r.
    destruct x as [a b].
    apply refl.
Defined.

Definition pair_uniqueness {A B : Type} {z : A * B} : z == (fst z, snd z).
Proof.
    apply pair_identity.
    exact (refl (fst z), refl (snd z)).
Defined.

(** Theorem 2.6.4 *)

Definition transport_product {Z} {A B : Z -> Type} {z w : Z} {p : z == w} {x : A z * B z} :
    transport (P := fun x => (A x * B x)%type) p x == (transport p (fst x), transport p (snd x)).
Proof.
    induction p.
    simpl.
    apply pair_uniqueness.
Defined.

(** Theorem 2.7.2 *)

Definition sig_identity_inv {A} {P : A -> Type} {x y : sigT P} :
    (x == y) -> { p : projT1 x == projT1 y & transport p (projT2 x) == projT2 y }.
Proof.
    intro p.
    exists (ap (@projT1 A P) p).
    induction p.
    apply refl.
Defined.

Definition sig_identity {A} {P : A -> Type} {x y : sigT P} :
    { p : projT1 x == projT1 y & transport p (projT2 x) == projT2 y } -> (x == y).
Proof.
    intro H.
    destruct H as [p q].
    destruct x as [a b].
    destruct y as [a' b'].
    simpl in p.
    induction p as [a].
    simpl in q.
    induction q.
    apply refl.
Defined.

Definition sig_identity_equiv {A} {P : A -> Type} {x y : sigT P} :
    (x == y) <~> { p : projT1 x == projT1 y & transport p (projT2 x) == projT2 y }.
Proof.
    exists sig_identity_inv.
    apply qinv_implies_equiv.
    exists sig_identity.
    split.
    intro H.
    destruct H as [p q].
    destruct x as [a b].
    destruct y as [a' b'].
    simpl in * |- *.
    induction p.
    simpl in q.
    induction q.
    apply refl.
    intro p.
    induction p.
    destruct x as [a b].
    apply refl.
Defined.

Definition sig_uniqueness {A} {P : A -> Type} {z : sigT P} : z == existT P (projT1 z) (projT2 z).
Proof.
    apply sig_identity.
    exact (existT _ (refl (projT1 z)) (refl (projT2 z))).
Defined.

(** Theorem 2.7.4 *)

Definition transport_sig {A} {P : A -> Type} {Q : sigT P -> Type} {x y : A} {p : x == y}
    {w : {u : P x & Q (existT P x u)}} :
    transport (P := fun x => {u : P x & Q (existT P x u)}) p w ==
    existT (fun u => Q (existT P y u)) (transport p (projT1 w))
           (transport (sig_identity (x := existT P x (projT1 w))
                                    (y := existT P y (transport p (projT1 w)))
                                    (existT _ p (refl (transport p (projT1 w)))))
                      (projT2 w)).
Proof.
    induction p.
    simpl.
    apply sig_uniqueness.
Defined.

(** Theorem 2.8.1 *)

Definition unit_identity_inv {x y : unit} : x == y -> unit := fun _ => tt.

Definition unit_identity {x y : unit} : unit -> x == y.
Proof.
    intro H.
    induction x.
    induction y.
    apply refl.
Defined.

Definition unit_identity_equiv {x y : unit} : x == y <~> unit.
Proof.
    exists unit_identity_inv.
    apply qinv_implies_equiv.
    exists unit_identity.
    split.
    intro H.
    induction H.
    apply refl.
    intro p.
    induction p.
    induction x.
    apply refl.
Defined.

Definition unit_uniqueness {x y : unit} : x == y.
Proof.
    exact (unit_identity tt).
Defined.

(** Definition 2.9.2 *)

Definition happly {A} {P : A -> Type} {f g : forall x, P x} : (f == g) -> (f ~~ g).
Proof.
    intro p.
    induction p.
    apply homotopy_refl.
Defined.

(** Axiom 2.9.3 *)

Axiom FunctionExtensionality :
    forall A (P : A -> Type) (f g : forall x, P x), is_equiv (@happly A P f g).

Definition funext {A} {P : A -> Type} {f g : forall x, P x} : (f ~~ g) -> (f == g).
Proof.
    exact (projT1 (equiv_implies_qinv (FunctionExtensionality A P f g))).
Defined.

Definition fun_uniqueness {A} {P : A -> Type} {f g : forall x : A, P x} {p : f == g} :
    p == funext (happly p).
Proof.
    pose (h := snd (projT2 (equiv_implies_qinv (FunctionExtensionality A P f g)))).
    exact (!(h p)).
Defined.

(** Lemma 2.9.4 *)

Definition transport_fun {X} {A B : X -> Type} {x y : X} {p : x == y} {f : A x -> B x} :
    transport (P := fun x => A x -> B x) p f == fun x => transport p (f (transport (!p) x)).
Proof.
    induction p.
    simpl.
    apply refl.
Defined.

(** Definition 2.10.1 *)

Definition id_to_equiv {A B : Type} : (A == B) -> (A <~> B).
Proof.
    intro p.
    exists (transport (P := fun (X : Type) => X) p).
    induction p as [A].
    apply id_equiv. 
Defined.

(** Axiom 2.10.3 *)

Axiom Univalence : forall A B, is_equiv (@id_to_equiv A B).

Definition ua {A B : Type} : (A <~> B) -> (A == B).
Proof.
    exact (projT1 (equiv_implies_qinv (Univalence A B))).
Defined.

(** Theorem 2.15.2 *)

Definition product_up {X A B} : (X -> A * B) <~> ((X -> A) * (X -> B)).
Proof.
    exists (fun f => ((@fst A B) o f, (@snd A B) o f)).
    apply qinv_implies_equiv.
    exists (fun w => match w with (g, h) => (fun x => (g x, h x)) end).
    split.
    intro w.
    destruct w as [g h].
    apply pair_identity.
    simpl.
    split; apply funext; intro x; apply refl. 
    intro f.
    simpl.
    apply funext.
    intro x.
    apply inverse, pair_uniqueness.
Defined.