From 2748525c21f59e186188e37e202cdfb59c9bb322 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 17 Jun 2015 19:31:05 -0400
Subject: [PATCH] feat(hit/susp): finish the proof that loop space is adjoint
 to the suspension

---
 hott/hit/susp.hlean      | 294 ++++++++++++++-------------------------
 hott/init/path.hlean     |   4 +-
 hott/types/eq.hlean      |  58 +++++---
 hott/types/pointed.hlean |  85 ++++++++---
 hott/types/trunc.hlean   |   2 +-
 5 files changed, 214 insertions(+), 229 deletions(-)

diff --git a/hott/hit/susp.hlean b/hott/hit/susp.hlean
index 29dbb6e6f..3b456666a 100644
--- a/hott/hit/susp.hlean
+++ b/hott/hit/susp.hlean
@@ -27,10 +27,10 @@ namespace susp
   protected definition rec {P : susp A → Type} (PN : P north) (PS : P south)
     (Pm : Π(a : A), PN =[merid a] PS) (x : susp A) : P x :=
   begin
-    fapply pushout.rec_on _ _ x,
-    { intro u, cases u, exact PN},
-    { intro u, cases u, exact PS},
-    { exact Pm},
+    induction x with u u,
+    { cases u, exact PN},
+    { cases u, exact PS},
+    { apply Pm},
   end
 
   protected definition rec_on [reducible] {P : susp A → Type} (y : susp A)
@@ -80,15 +80,17 @@ attribute susp.elim_type_on [unfold-c 2]
 namespace susp
   open pointed
 
-  definition pointed_susp [instance] [constructor] (A : Type) : pointed (susp A) :=
+  variables {X Y Z : Pointed}
+
+  definition pointed_susp [instance] [constructor] (X : Type) : pointed (susp X) :=
   pointed.mk north
 
-  definition Susp [constructor] (A : Type) : Pointed :=
-  pointed.mk' (susp A)
+  definition Susp [constructor] (X : Type) : Pointed :=
+  pointed.mk' (susp X)
 
-  definition Susp_functor {X Y : Pointed} (f : X →* Y) : Susp X →* Susp Y :=
+  definition Susp_functor (f : X →* Y) : Susp X →* Susp Y :=
   begin
-    fapply pmap.mk,
+    constructor,
     { intro x, induction x,
         apply north,
         apply south,
@@ -96,10 +98,10 @@ namespace susp
     { reflexivity}
   end
 
-  definition Susp_functor_compose {X Y Z : Pointed} (g : Y →* Z) (f : X →* Y)
+  definition Susp_functor_compose (g : Y →* Z) (f : X →* Y)
     : Susp_functor (g ∘* f) ~* Susp_functor g ∘* Susp_functor f :=
   begin
-    fapply phomotopy.mk,
+    constructor,
     { intro a, induction a,
       { reflexivity},
       { reflexivity},
@@ -112,198 +114,116 @@ namespace susp
 
   definition loop_susp_unit [constructor] (X : Pointed) : X →* Ω(Susp X) :=
   begin
-    fapply pmap.mk,
+    constructor,
     { intro x, exact merid x ⬝ (merid pt)⁻¹},
     { apply con.right_inv},
   end
 
-  definition loop_susp_unit_natural {X Y : Pointed} (f : X →* Y)
+  definition loop_susp_unit_natural (f : X →* Y)
     : loop_susp_unit Y ∘* f ~* ap1 (Susp_functor f) ∘* loop_susp_unit X :=
   begin
     induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
-    fapply phomotopy.mk,
-    { intro x', esimp [Susp_functor],
-      refine _ ⬝ !idp_con⁻¹,
-      refine _ ⬝ !ap_con⁻¹,
-      exact (!elim_merid ◾ (!ap_inv ⬝ inverse2 !elim_merid))⁻¹},
+    constructor,
+    { intro x', esimp [Susp_functor], symmetry,
+      exact
+        !idp_con ⬝
+        (!ap_con ⬝
+        whisker_left _ !ap_inv) ⬝
+        (!elim_merid ◾ (inverse2 !elim_merid))
+        },
     { rewrite [▸*,idp_con (con.right_inv _)],
-      exact sorry}, --apply inv_con_eq_of_eq_con,
+      apply inv_con_eq_of_eq_con,
+      refine _ ⬝ !con.assoc',
+      rewrite inverse2_right_inv,
+      refine _ ⬝ !con.assoc',
+      rewrite [ap_con_right_inv,↑Susp_functor,idp_con_idp,-ap_compose]},
   end
 
--- p ⬝ q ⬝ r means (p ⬝ q) ⬝ r
+  definition loop_susp_counit [constructor] (X : Pointed) : Susp (Ω X) →* X :=
+  begin
+    constructor,
+    { intro x, induction x, exact pt, exact pt, exact a},
+    { reflexivity},
+  end
 
-  definition susp_adjoint_loop (A B : Pointed)
-    : map₊ (pointed.mk' (susp A)) B ≃ map₊ A (Ω B) := sorry
+  definition loop_susp_counit_natural (f : X →* Y)
+    : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (Susp_functor (ap1 f)) :=
+  begin
+    induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
+    constructor,
+    { intro x', induction x' with p,
+      { reflexivity},
+      { reflexivity},
+      { esimp, apply pathover_eq, apply hdeg_square,
+        xrewrite [ap_compose _ f,ap_compose _ (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*,
+                  +elim_merid,▸*,idp_con]}},
+    { reflexivity}
+  end
 
-exit
+  definition loop_susp_counit_unit (X : Pointed)
+    : ap1 (loop_susp_counit X) ∘* loop_susp_unit (Ω X) ~* pid (Ω X) :=
+  begin
+    induction X with X x, constructor,
+    { intro p, esimp,
+      refine !idp_con ⬝
+             (!ap_con ⬝
+             whisker_left _ !ap_inv) ⬝
+             (!elim_merid ◾ inverse2 !elim_merid)},
+    { rewrite [▸*,inverse2_right_inv (elim_merid function.id idp)],
+      refine !con.assoc ⬝ _,
+      xrewrite [ap_con_right_inv (susp.elim x x (λa, a)) (merid idp),idp_con_idp,-ap_compose]}
+  end
 
-Definition loop_susp_unit_natural {X Y : pType} (f : X ->* Y)
-: loop_susp_unit Y o* f
-  ==* loops_functor (psusp_functor f) o* loop_susp_unit X.
-Proof.
-  pointed_reduce.
-  refine (Build_pHomotopy _ _); cbn.
-  - intros x; symmetry.
-    refine (concat_1p _@ (concat_p1 _ @ _)).
-    refine (ap_pp (Susp_rec North South (merid o f))
-                  (merid x) (merid (point X))^ @ _).
-    refine ((1 @@ ap_V _ _) @ _).
-    refine (Susp_comp_nd_merid _ @@ inverse2 (Susp_comp_nd_merid _)).
-  - cbn. rewrite !inv_pp, !concat_pp_p, concat_1p; symmetry.
-    apply moveL_Vp.
-    refine (concat_pV_inverse2 _ _ (Susp_comp_nd_merid (point X)) @ _).
-    do 2 apply moveL_Vp.
-    refine (ap_pp_concat_pV _ _ @ _).
-    do 2 apply moveL_Vp.
-    rewrite concat_p1_1, concat_1p_1.
-    cbn; symmetry.
-    refine (concat_p1 _ @ _).
-    refine (ap_compose (fun p' => (ap (Susp_rec North South (merid o f))) p' @ 1)
-                       (fun p' => 1 @ p')
-                       (concat_pV (merid (point X))) @ _).
-    apply ap.
-    refine (ap_compose (ap (Susp_rec North South (merid o f)))
-                       (fun p' => p' @ 1) _).
-Qed.
+  definition loop_susp_unit_counit (X : Pointed)
+    : loop_susp_counit (Susp X) ∘* Susp_functor (loop_susp_unit X) ~* pid (Susp X) :=
+  begin
+    induction X with X x, constructor,
+    { intro x', induction x',
+      { reflexivity},
+      { exact merid pt},
+      { apply pathover_eq,
+        xrewrite [▸*, ap_id, ap_compose _ (susp.elim north north (λa, a)), +elim_merid,▸*],
+        apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹}},
+    { reflexivity}
+  end
 
-Definition loop_susp_counit (X : pType) : psusp (loops X) ->* X.
-Proof.
-  refine (Build_pMap (psusp (loops X)) X
-                     (Susp_rec (point X) (point X) idmap) 1).
-Defined.
-
-Definition loop_susp_counit_natural {X Y : pType} (f : X ->* Y)
-: f o* loop_susp_counit X
-  ==* loop_susp_counit Y o* psusp_functor (loops_functor f).
-Proof.
-  pointed_reduce.
-  refine (Build_pHomotopy _ _); simpl.
-  - refine (Susp_ind _ _ _ _); cbn; try reflexivity; intros p.
-    rewrite transport_paths_FlFr, ap_compose, concat_p1.
-    apply moveR_Vp.
-    refine (ap_compose
-              (Susp_rec North South (fun x0 => merid (1 @ (ap f x0 @ 1))))
-              (Susp_rec (point Y) (point Y) idmap) (merid p) @ _).
-    do 2 rewrite Susp_comp_nd_merid.
-    refine (Susp_comp_nd_merid _ @ _). (** Not sure why [rewrite] fails here *)
-    apply concat_1p.
-  - reflexivity.
-Qed.
-
-(** Now the triangle identities *)
-
-Definition loop_susp_triangle1 (X : pType)
-: loops_functor (loop_susp_counit X) o* loop_susp_unit (loops X)
-  ==* pmap_idmap (loops X).
-Proof.
-  refine (Build_pHomotopy _ _).
-  - intros p; cbn.
-    refine (concat_1p _ @ (concat_p1 _ @ _)).
-    refine (ap_pp (Susp_rec (point X) (point X) idmap)
-                  (merid p) (merid (point (point X = point X)))^ @ _).
-    refine ((1 @@ ap_V _ _) @ _).
-    refine ((Susp_comp_nd_merid p @@ inverse2 (Susp_comp_nd_merid (point (loops X)))) @ _).
-    exact (concat_p1 _).
-  - destruct X as [X x]; cbn; unfold point.
-    apply whiskerR.
-    rewrite (concat_pV_inverse2
-               (ap (Susp_rec x x idmap) (merid 1))
-               1 (Susp_comp_nd_merid 1)).
-    rewrite (ap_pp_concat_pV (Susp_rec x x idmap) (merid 1)).
-    rewrite ap_compose, (ap_compose _ (fun p => p @ 1)).
-    rewrite concat_1p_1; apply ap.
-    apply concat_p1_1.
-Qed.
-
-Definition loop_susp_triangle2 (X : pType)
-: loop_susp_counit (psusp X) o* psusp_functor (loop_susp_unit X)
-  ==* pmap_idmap (psusp X).
-Proof.
-  refine (Build_pHomotopy _ _);
-  [ refine (Susp_ind _ _ _ _) | ]; try reflexivity; cbn.
-  - exact (merid (point X)).
-  - intros x.
-    rewrite transport_paths_FlFr, ap_idmap, ap_compose.
-    rewrite Susp_comp_nd_merid.
-    apply moveR_pM; rewrite concat_p1.
-    refine (inverse2 (Susp_comp_nd_merid _) @ _).
-    rewrite inv_pp, inv_V; reflexivity.
-Qed.
-
-(** Now we can finally construct the adjunction equivalence. *)
-
-Definition loop_susp_adjoint `{Funext} (A B : pType)
-: (psusp A ->* B) <~> (A ->* loops B).
-Proof.
-  refine (equiv_adjointify
-            (fun f => loops_functor f o* loop_susp_unit A)
-            (fun g => loop_susp_counit B o* psusp_functor g) _ _).
-  - intros g. apply path_pmap.
-    refine (pmap_prewhisker _ (loops_functor_compose _ _) @* _).
-    refine (pmap_compose_assoc _ _ _ @* _).
-    refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _).
-    refine ((pmap_compose_assoc _ _ _)^* @* _).
-    refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _).
-    apply pmap_postcompose_idmap.
-  - intros f. apply path_pmap.
-    refine (pmap_postwhisker _ (psusp_functor_compose _ _) @* _).
-    refine ((pmap_compose_assoc _ _ _)^* @* _).
-    refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _).
-    refine (pmap_compose_assoc _ _ _ @* _).
-    refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _).
-    apply pmap_precompose_idmap.
-Defined.
-
-(** And its naturality is easy. *)
-
-Definition loop_susp_adjoint_nat_r `{Funext} (A B B' : pType)
-           (f : psusp A ->* B) (g : B ->* B')
-: loop_susp_adjoint A B' (g o* f)
-  ==* loops_functor g o* loop_susp_adjoint A B f.
-Proof.
-  cbn.
-  refine (_ @* pmap_compose_assoc _ _ _).
-  apply pmap_prewhisker.
-  refine (loops_functor_compose g f).
-Defined.
-
-Definition loop_susp_adjoint_nat_l `{Funext} (A A' B : pType)
-           (f : A ->* loops B) (g : A' ->* A)
-: (loop_susp_adjoint A' B)^-1 (f o* g)
-  ==* (loop_susp_adjoint A B)^-1 f o* psusp_functor g.
-Proof.
-  cbn.
-  refine (_ @* (pmap_compose_assoc _ _ _)^*).
-  apply pmap_postwhisker.
-  refine (psusp_functor_compose f g).
-Defined.
-
-
-
-  definition susp_adjoint_loop (A B : Pointed)
-    : map₊ (pointed.mk' (susp A)) B ≃ map₊ A (Ω B) :=
+  definition susp_adjoint_loop (X Y : Pointed) : map₊ (pointed.mk' (susp X)) Y ≃ map₊ X (Ω Y) :=
   begin
     fapply equiv.MK,
-    { intro f, fapply pointed_map.mk,
-       intro a, refine !respect_pt⁻¹ ⬝ ap f (merid a ⬝ (merid pt)⁻¹) ⬝ !respect_pt,
-       refine ap _ !con.right_inv ⬝ !con.left_inv},
-    { intro g, fapply pointed_map.mk,
-      { esimp, intro a, induction a,
-          exact pt,
-          exact pt,
-          exact g a} ,
-      { reflexivity}},
-    { intro g, fapply pointed_map_eq,
-        intro a, esimp [respect_pt], refine !idp_con ⬝ !ap_con ⬝ ap _ !ap_inv
-           ⬝ ap _ !elim_merid ⬝ ap _ !elim_merid ⬝ ap _ (respect_pt g) ⬝ _, exact idp,
-        -- rewrite [ap_con,ap_inv,+elim_merid,idp_con,respect_pt],
-       esimp, exact sorry},
-    { intro f, fapply pointed_map_eq,
-      { esimp, intro a, induction a; all_goals esimp,
-          exact !respect_pt⁻¹,
-          exact !respect_pt⁻¹ ⬝ ap f (merid pt),
-          apply pathover_eq, exact sorry},
-      { esimp, exact !con.left_inv⁻¹}},
+    { intro f, exact ap1 f ∘* loop_susp_unit X},
+    { intro g, exact loop_susp_counit Y ∘* Susp_functor g},
+    { intro g, apply eq_of_phomotopy, esimp,
+      refine !pwhisker_right !ap1_compose ⬝* _,
+      refine !passoc ⬝* _,
+      refine !pwhisker_left !loop_susp_unit_natural⁻¹* ⬝* _,
+      refine !passoc⁻¹* ⬝* _,
+      refine !pwhisker_right !loop_susp_counit_unit ⬝* _,
+      apply pid_comp},
+    { intro f, apply eq_of_phomotopy, esimp,
+      refine !pwhisker_left !Susp_functor_compose ⬝* _,
+      refine !passoc⁻¹* ⬝* _,
+      refine !pwhisker_right !loop_susp_counit_natural⁻¹* ⬝* _,
+      refine !passoc ⬝* _,
+      refine !pwhisker_left !loop_susp_unit_counit ⬝* _,
+      apply comp_pid},
+  end
+
+  definition susp_adjoint_loop_nat_right (f : Susp X →* Y) (g : Y →* Z)
+    : susp_adjoint_loop X Z (g ∘* f) ~* ap1 g ∘* susp_adjoint_loop X Y f :=
+  begin
+    esimp [susp_adjoint_loop],
+    refine _ ⬝* !passoc,
+    apply pwhisker_right,
+    apply ap1_compose
+  end
+
+  definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y)
+    : (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* Susp_functor g :=
+  begin
+    esimp [susp_adjoint_loop],
+    refine _ ⬝* !passoc⁻¹*,
+    apply pwhisker_left,
+    apply Susp_functor_compose
   end
 
 end susp
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 7a8005029..72789880f 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -63,11 +63,11 @@ namespace eq
   eq.rec_on r (eq.rec_on q idp)
 
   -- The left inverse law.
-  definition con.right_inv (p : x = y) : p ⬝ p⁻¹ = idp :=
+  definition con.right_inv [unfold-c 4] (p : x = y) : p ⬝ p⁻¹ = idp :=
   eq.rec_on p idp
 
   -- The right inverse law.
-  definition con.left_inv (p : x = y) : p⁻¹ ⬝ p = idp :=
+  definition con.left_inv [unfold-c 4] (p : x = y) : p⁻¹ ⬝ p = idp :=
   eq.rec_on p idp
 
   /- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean
index 0854b974d..769785105 100644
--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@@ -15,50 +15,64 @@ namespace eq
   /- Path spaces -/
 
   variables {A B : Type} {a a1 a2 a3 a4 : A} {b b1 b2 : B} {f g : A → B} {h : B → A}
+            {p p' p'' : a1 = a2}
 
   /- The path spaces of a path space are not, of course, determined; they are just the
       higher-dimensional structure of the original space. -/
 
   /- some lemmas about whiskering or other higher paths -/
 
-  definition whisker_left_con_right (p : a1 = a2) {q q' q'' : a2 = a3} (r : q = q') (s : q' = q'')
+  theorem whisker_left_con_right (p : a1 = a2) {q q' q'' : a2 = a3} (r : q = q') (s : q' = q'')
     : whisker_left p (r ⬝ s) = whisker_left p r ⬝ whisker_left p s :=
   begin
-    cases p, cases r, cases s, exact idp
+    cases p, cases r, cases s, reflexivity
   end
 
-  definition whisker_right_con_right {p p' p'' : a1 = a2} (q : a2 = a3) (r : p = p') (s : p' = p'')
+  theorem whisker_right_con_right (q : a2 = a3) (r : p = p') (s : p' = p'')
     : whisker_right (r ⬝ s) q = whisker_right r q ⬝ whisker_right s q :=
   begin
-    cases q, cases r, cases s, exact idp
+    cases q, cases r, cases s, reflexivity
   end
 
-  definition whisker_left_con_left (p : a1 = a2) (p' : a2 = a3) {q q' : a3 = a4} (r : q = q')
+  theorem whisker_left_con_left (p : a1 = a2) (p' : a2 = a3) {q q' : a3 = a4} (r : q = q')
     : whisker_left (p ⬝ p') r = !con.assoc ⬝ whisker_left p (whisker_left p' r) ⬝ !con.assoc' :=
   begin
-    cases p', cases p, cases r, cases q, exact idp
+    cases p', cases p, cases r, cases q, reflexivity
   end
 
-  definition whisker_right_con_left {p p' : a1 = a2} (q : a2 = a3) (q' : a3 = a4) (r : p = p')
+  theorem whisker_right_con_left {p p' : a1 = a2} (q : a2 = a3) (q' : a3 = a4) (r : p = p')
     : whisker_right r (q ⬝ q') = !con.assoc' ⬝ whisker_right (whisker_right r q) q' ⬝ !con.assoc :=
   begin
-    cases q', cases q, cases r, cases p, exact idp
+    cases q', cases q, cases r, cases p, reflexivity
   end
 
-  definition whisker_left_inv_left (p : a2 = a1) {q q' : a2 = a3} (r : q = q')
+  theorem whisker_left_inv_left (p : a2 = a1) {q q' : a2 = a3} (r : q = q')
     : !con_inv_cancel_left⁻¹ ⬝ whisker_left p (whisker_left p⁻¹ r) ⬝ !con_inv_cancel_left = r :=
   begin
-    cases p, cases r, cases q, exact idp
+    cases p, cases r, cases q, reflexivity
   end
 
-  definition con_right_inv2 (p : a1 = a2) : (con.right_inv p)⁻¹ ⬝ con.right_inv p = idp :=
-  by cases p;exact idp
+  theorem ap_eq_ap10 {f g : A → B} (p : f = g) (a : A) : ap (λh, h a) p = ap10 p a :=
+  by cases p;reflexivity
 
-  definition con_left_inv2 (p : a1 = a2) : (con.left_inv p)⁻¹ ⬝ con.left_inv p = idp :=
-  by cases p;exact idp
+  theorem inverse2_right_inv (r : p = p') : r ◾ inverse2 r ⬝ con.right_inv p' = con.right_inv p :=
+  by cases r;cases p;reflexivity
 
-  definition ap_eq_ap10 {f g : A → B} (p : f = g) (a : A) : ap (λh, h a) p = ap10 p a :=
-  by cases p;exact idp
+  theorem inverse2_left_inv (r : p = p') : inverse2 r ◾ r ⬝ con.left_inv p' = con.left_inv p :=
+  by cases r;cases p;reflexivity
+
+  theorem ap_con_right_inv (f : A → B) (p : a1 = a2)
+    : ap_con f p p⁻¹ ⬝ whisker_left _ (ap_inv f p) ⬝ con.right_inv (ap f p)
+      = ap (ap f) (con.right_inv p) :=
+  by cases p;reflexivity
+
+  theorem ap_con_left_inv (f : A → B) (p : a1 = a2)
+    : ap_con f p⁻¹ p ⬝ whisker_right (ap_inv f p) _ ⬝ con.left_inv (ap f p)
+      = ap (ap f) (con.left_inv p) :=
+  by cases p;reflexivity
+
+  theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q :=
+  by cases q;reflexivity
 
   /- Transporting in path spaces.
 
@@ -177,7 +191,7 @@ namespace eq
   is_equiv.mk (concat p) (concat p⁻¹)
               (con_inv_cancel_left p)
               (inv_con_cancel_left p)
-              (λq, by cases p;cases q;exact idp)
+              (λq, by cases p;cases q;reflexivity)
   local attribute is_equiv_concat_left [instance]
 
   definition equiv_eq_closed_left [constructor] (a3 : A) (p : a1 = a2) : (a1 = a3) ≃ (a2 = a3) :=
@@ -188,7 +202,7 @@ namespace eq
   is_equiv.mk (λq, q ⬝ p) (λq, q ⬝ p⁻¹)
               (λq, inv_con_cancel_right q p)
               (λq, con_inv_cancel_right q p)
-              (λq, by cases p;cases q;exact idp)
+              (λq, by cases p;cases q;reflexivity)
   local attribute is_equiv_concat_right [instance]
 
   definition equiv_eq_closed_right [constructor] (a1 : A) (p : a2 = a3) : (a1 = a2) ≃ (a1 = a3) :=
@@ -208,10 +222,10 @@ namespace eq
       apply concat2,
         {apply concat, {apply whisker_left_con_right},
           apply concat2,
-            {cases p, cases q, exact idp},
-            {exact idp}},
-        {cases p, cases r, exact idp}},
-    {intro s, cases s, cases q, cases p, exact idp}
+            {cases p, cases q, reflexivity},
+            {reflexivity}},
+        {cases p, cases r, reflexivity}},
+    {intro s, cases s, cases q, cases p, reflexivity}
   end
 
   definition eq_equiv_con_eq_con_left (p : a1 = a2) (q r : a2 = a3) : (q = r) ≃ (p ⬝ q = p ⬝ r) :=
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index fd19ff9a3..232256b79 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -30,7 +30,8 @@ namespace pointed
   pointed.mk (Point A)
 
   -- Any contractible type is pointed
-  definition pointed_of_is_contr [instance] [constructor] (A : Type) [H : is_contr A] : pointed A :=
+  definition pointed_of_is_contr [instance] [priority 800] [constructor]
+    (A : Type) [H : is_contr A] : pointed A :=
   pointed.mk !center
 
   -- A pi type with a pointed target is pointed
@@ -99,15 +100,13 @@ open pmap
 
 namespace pointed
 
-  variables {A B C D : Pointed}
-
   abbreviation respect_pt [unfold-c 3] := @pmap.resp_pt
-
   notation `map₊` := pmap
   infix `→*`:30 := pmap
   attribute pmap.map [coercion]
-  definition pmap_eq {f g : map₊ A B}
-    (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g :=
+  variables {A B C D : Pointed} {f g h : A →* B}
+
+  definition pmap_eq (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g :=
   begin
     cases f with f p, cases g with g q,
     esimp at *,
@@ -131,22 +130,36 @@ namespace pointed
 
   infix `~*`:50 := phomotopy
   abbreviation to_homotopy_pt [unfold-c 5] := @phomotopy.homotopy_pt
-  abbreviation to_homotopy [coercion] [unfold-c 5] {f g : A →* B} (p : f ~* g) : Πa, f a = g a :=
+  abbreviation to_homotopy [coercion] [unfold-c 5] (p : f ~* g) : Πa, f a = g a :=
   phomotopy.homotopy p
 
   definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) :=
   begin
-    fapply phomotopy.mk, intro a, reflexivity,
+    constructor, intro a, reflexivity,
     cases A, cases B, cases C, cases D, cases f with f pf, cases g with g pg, cases h with h ph,
     esimp at *,
     induction pf, induction pg, induction ph, reflexivity
   end
 
+  definition pid_comp (f : A →* B) : pid B ∘* f ~* f :=
+  begin
+    constructor,
+    { intro a, reflexivity},
+    { esimp, exact !idp_con ⬝ !ap_id⁻¹}
+  end
+
+  definition comp_pid (f : A →* B) : f ∘* pid A ~* f :=
+  begin
+    constructor,
+    { intro a, reflexivity},
+    { reflexivity}
+  end
+
   definition pmap_equiv_left (A : Type) (B : Pointed) : A₊ →* B ≃ (A → B) :=
   begin
     fapply equiv.MK,
     { intro f a, cases f with f p, exact f (some a)},
-    { intro f, fapply pmap.mk,
+    { intro f, constructor,
         intro a, cases a, exact pt, exact f a,
         reflexivity},
     { intro f, reflexivity},
@@ -180,7 +193,7 @@ namespace pointed
   begin
     fapply equiv.MK,
     { intro f, cases f with f p, exact f tt},
-    { intro b, fapply pmap.mk,
+    { intro b, constructor,
         intro u, cases u, exact pt, exact b,
         reflexivity},
     { intro b, reflexivity},
@@ -196,37 +209,75 @@ namespace pointed
   { intros A B f, rewrite [↑Iterated_loop_space,↓Iterated_loop_space n (Ω A),
       ↑Iterated_loop_space, ↓Iterated_loop_space n (Ω B)],
     apply IH (Ω A),
-    { esimp, fapply pmap.mk,
+    { esimp, constructor,
         intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt,
         esimp, apply con.left_inv}}
   end
 
-  definition ap1 [constructor] (f : A →* B) := apn (succ 0) f
+  definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := apn (succ 0) f
 
-  protected definition phomotopy.trans [trans] {f g h : A →* B} (p : f ~* g) (q : g ~* h)
+  definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
+  begin
+    induction B, induction C, induction g with g pg, induction f with f pf, esimp at *,
+    induction pg, induction pf,
+    constructor,
+    { intro p, esimp, apply whisker_left, exact ap_compose f g p ⬝ ap (ap g) !idp_con⁻¹},
+    { reflexivity}
+  end
+
+  protected definition phomotopy.refl [refl] (f : A →* B) : f ~* f :=
+  begin
+    constructor,
+    { intro a, exact idp},
+    { apply idp_con}
+  end
+
+  protected definition phomotopy.trans [trans] (p : f ~* g) (q : g ~* h)
     : f ~* h :=
   begin
-    fapply phomotopy.mk,
+    constructor,
     { intro a, exact p a ⬝ q a},
     { induction f, induction g, induction p with p p', induction q with q q', esimp at *,
       induction p', induction q', esimp, apply con.assoc}
   end
 
-  protected definition phomotopy.symm [symm] {f g : A →* B} (p : f ~* g) : g ~* f :=
+  protected definition phomotopy.symm [symm] (p : f ~* g) : g ~* f :=
   begin
-    fapply phomotopy.mk,
+    constructor,
     { intro a, exact (p a)⁻¹},
     { induction f, induction p with p p', esimp at *,
       induction p', esimp, apply inv_con_cancel_left}
   end
 
-  definition eq_of_phomotopy {f g : A →* B} (p : f ~* g) : f = g :=
+  infix `⬝*`:75 := phomotopy.trans
+  postfix `⁻¹*`:(max+1) := phomotopy.symm
+
+  definition eq_of_phomotopy (p : f ~* g) : f = g :=
   begin
     fapply pmap_eq,
     { intro a, exact p a},
     { exact !to_homotopy_pt⁻¹}
   end
 
+  definition pwhisker_left (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g :=
+  begin
+    constructor,
+    { intro a, exact ap h (p a)},
+    { induction A, induction B, induction C,
+      induction f with f pf, induction g with g pg, induction h with h ph,
+      induction p with p p', esimp at *, induction ph, induction pg, induction p', reflexivity}
+  end
+
+  definition pwhisker_right (h : C →* A) (p : f ~* g) : f ∘* h ~* g ∘* h :=
+  begin
+    constructor,
+    { intro a, exact p (h a)},
+    { induction A, induction B, induction C,
+      induction f with f pf, induction g with g pg, induction h with h ph,
+      induction p with p p', esimp at *, induction ph, induction pg, induction p', esimp,
+      exact !idp_con⁻¹}
+  end
+
   structure pequiv (A B : Pointed) :=
     (to_pmap : A →* B)
     (is_equiv_to_pmap : is_equiv to_pmap)
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index e62111265..496b3ef37 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -165,7 +165,7 @@ namespace is_trunc
           { esimp, transitivity _,
             apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹),
             esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv},
-          { esimp, apply con_right_inv2}},
+          { esimp, apply con.left_inv}},
         transitivity _,
           apply iff.pi_iff_pi, intro p,
           rewrite [↑Iterated_loop_space,↓Iterated_loop_space n (Loop_space (pointed.Mk p)),H],