generalize many results about pointed homotopies of nondependent maps to dependent maps

hott/init/funext.hlean

@@ -285,6 +285,25 @@ namespace eq
     induction p using homotopy.rec_on, induction q, exact H
   end
 
+  definition homotopy.rec_idp [recursor] {A : Type} {P : A → Type} {f : Πa, P a}
+    (Q : Π{g}, (f ~ g) → Type) (H : Q (homotopy.refl f)) {g : Π x, P x} (p : f ~ g) : Q p :=
+  homotopy.rec_on_idp p H
+
+  definition homotopy_rec_on_apd10 {A : Type} {P : A → Type} {f g : Πa, P a}
+    (Q : f ~ g → Type) (H : Π(q : f = g), Q (apd10 q)) (p : f = g) :
+    homotopy.rec_on (apd10 p) H = H p :=
+  begin
+    unfold [homotopy.rec_on],
+    refine ap (λp, p ▸ _) !adj ⬝ _,
+    refine !tr_compose⁻¹ ⬝ _,
+    apply apdt
+  end
+
+  definition homotopy_rec_idp_refl {A : Type} {P : A → Type} {f : Πa, P a}
+    (Q : Π{g}, f ~ g → Type) (H : Q homotopy.rfl) :
+    homotopy.rec_idp @Q H homotopy.rfl = H :=
+  !homotopy_rec_on_apd10
+
   definition eq_of_homotopy_inv {f g : Π x, P x} (H : f ~ g)
     : eq_of_homotopy (λx, (H x)⁻¹) = (eq_of_homotopy H)⁻¹ :=
   begin

hott/init/pathover.hlean

@@ -82,6 +82,9 @@ namespace eq
   definition change_path [unfold 9] (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ :=
   q ▸ r
 
+  definition change_path_idp [unfold_full] (r : b =[p] b₂) : change_path idp r = r :=
+  by reflexivity
+
   -- infix ` ⬝ ` := concato
   infix ` ⬝o `:72 := concato
   infix ` ⬝op `:73 := concato_eq
@@ -103,25 +106,25 @@ namespace eq
 
   /- Some of the theorems analogous to theorems for = in init.path -/
 
-  definition cono_idpo (r : b =[p] b₂) : r ⬝o idpo =[con_idp p] r :=
+  definition cono_idpo (r : b =[p] b₂) : r ⬝o idpo = r :=
-  pathover.rec_on r idpo
+  by reflexivity
 
   definition idpo_cono (r : b =[p] b₂) : idpo ⬝o r =[idp_con p] r :=
-  pathover.rec_on r idpo
+  by induction r; constructor
 
   definition cono.assoc' (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) :
     r ⬝o (r₂ ⬝o r₃) =[!con.assoc'] (r ⬝o r₂) ⬝o r₃ :=
-  pathover.rec_on r₃ (pathover.rec_on r₂ (pathover.rec_on r idpo))
+  by induction r₃; constructor
 
   definition cono.assoc (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) :
     (r ⬝o r₂) ⬝o r₃ =[!con.assoc] r ⬝o (r₂ ⬝o r₃) :=
-  pathover.rec_on r₃ (pathover.rec_on r₂ (pathover.rec_on r idpo))
+  by induction r₃; constructor
 
   definition cono.right_inv (r : b =[p] b₂) : r ⬝o r⁻¹ᵒ =[!con.right_inv] idpo :=
-  pathover.rec_on r idpo
+  by induction r; constructor
 
   definition cono.left_inv (r : b =[p] b₂) : r⁻¹ᵒ ⬝o r =[!con.left_inv] idpo :=
-  pathover.rec_on r idpo
+  by induction r; constructor
 
   definition eq_of_pathover {a' a₂' : A'} (q : a' =[p] a₂') : a' = a₂' :=
   by cases q;reflexivity
@@ -159,6 +162,11 @@ namespace eq
     eq_of_pathover_idp (pathover_of_eq (idpath x) p) = p :=
   by induction p; reflexivity
 
+  variable (B)
+  definition idpo_concato_eq (r : b = b') : eq_of_pathover_idp (@idpo A B a b ⬝op r) = r :=
+  by induction r; reflexivity
+  variable {B}
+
   -- definition pathover_idp (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' :=
   -- pathover_equiv_tr_eq idp b b'
 
@@ -245,6 +253,9 @@ namespace eq
   definition apd [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ :=
   by induction p; constructor
 
+  definition apd_idp [unfold_full] (f : Πa, B a) : apd f idp = @idpo A B a (f a) :=
+  by reflexivity
+
   definition apo [unfold 12] {f : A → A'} (g : Πa, B a → B'' (f a)) (q : b =[p] b₂) :
     g a b =[p] g a₂ b₂ :=
   by induction q; constructor
@@ -388,19 +399,19 @@ namespace eq
 
   definition cono.right_inv_eq (q : b = b') :
     pathover_idp_of_eq q ⬝op q⁻¹ = (idpo : b =[refl a] b) :=
-  by induction q;constructor
+  by induction q; constructor
 
   definition cono.right_inv_eq' (q : b = b') :
     q ⬝po (pathover_idp_of_eq q⁻¹) = (idpo : b =[refl a] b) :=
-  by induction q;constructor
+  by induction q; constructor
 
   definition cono.left_inv_eq (q : b = b') :
     pathover_idp_of_eq q⁻¹ ⬝op q = (idpo : b' =[refl a] b') :=
-  by induction q;constructor
+  by induction q; constructor
 
   definition cono.left_inv_eq' (q : b = b') :
     q⁻¹ ⬝po pathover_idp_of_eq q = (idpo : b' =[refl a] b') :=
-  by induction q;constructor
+  by induction q; constructor
 
   definition pathover_of_fn_pathover_fn (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ :=
   (left_inv f b)⁻¹ ⬝po apo (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂

hott/init/pointed.hlean

@@ -88,31 +88,26 @@ structure ppi {A : Type*} (P : A → Type) (x₀ : P pt) :=
   (to_fun : Π a : A, P a)
   (resp_pt : to_fun (Point A) = x₀)
 
-definition ppi_const [constructor] {A : Type*} (P : A → Type*) : ppi P pt :=
-ppi.mk (λa, pt) idp
-
 definition pppi' [reducible] {A : Type*} (P : A → Type*) : Type :=
 ppi P pt
 
+definition ppi_const [constructor] {A : Type*} (P : A → Type*) : pppi' P :=
+ppi.mk (λa, pt) idp
+
 definition pppi [constructor] [reducible] {A : Type*} (P : A → Type*) : Type* :=
 pointed.MK (pppi' P) (ppi_const P)
 
+-- do we want to make this already pointed?
+definition pmap [reducible] (A B : Type*) : Type := @pppi A (λa, B)
+
+attribute ppi.to_fun [coercion]
+
+infix ` →* `:28 := pmap
 notation `Π*` binders `, ` r:(scoped P, pppi P) := r
 
--- We could try to define pmap as a special case of ppi
--- definition pmap' (A B : Type*) : Type := @pppi' A (λa, B)
--- todo: make this already pointed?
-definition pmap [reducible] (A B : Type*) : Type := @pppi A (λa, B)
--- structure pmap (A B : Type*) :=
---   (to_fun : A → B)
---   (resp_pt : to_fun (Point A) = Point B)
 
 namespace pointed
 
-  attribute ppi.to_fun [coercion]
-
-  notation `map₊` := pmap
-  infix ` →* `:28 := pmap
 
   definition pppi.mk [constructor] [reducible] {A : Type*} {P : A → Type*} (f : Πa, P a)
     (p : f pt = pt) : pppi P :=
@@ -126,7 +121,7 @@ namespace pointed
     (p : f (Point A) = Point B) : A →* B :=
 	pppi.mk f p
 
-  definition pmap.to_fun [unfold 3] [reducible] {A B : Type*} (f : A →* B) : A → B :=
+  abbreviation pmap.to_fun [unfold 3] [reducible] [coercion] {A B : Type*} (f : A →* B) : A → B :=
   pppi.to_fun f
 
   definition respect_pt [unfold 4] [reducible] {A : Type*} {P : A → Type} {p₀ : P pt}

hott/types/pointed.hlean

@@ -116,10 +116,10 @@ namespace pointed
 
   /- categorical properties of pointed maps -/
 
-  definition pid [constructor] (A : Type*) : A →* A :=
+  definition pid [constructor] [refl] (A : Type*) : A →* A :=
   pmap.mk id idp
 
-  definition pcompose [constructor] {A B C : Type*} (g : B →* C) (f : A →* B) : A →* C :=
+  definition pcompose [constructor] [trans] {A B C : Type*} (g : B →* C) (f : A →* B) : A →* C :=
   pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g)
 
   infixr ` ∘* `:60 := pcompose
@@ -323,7 +323,7 @@ namespace pointed
   protected definition phomotopy.refl [constructor] : k ~* k :=
   phomotopy.mk homotopy.rfl !idp_con
   variable {k}
-  protected definition phomotopy.rfl [constructor] [refl] : k ~* k :=
+  protected definition phomotopy.rfl [reducible] [constructor] [refl] : k ~* k :=
   phomotopy.refl k
 
   protected definition phomotopy.symm [constructor] [symm] (p : k ~* l) : l ~* k :=
@@ -447,8 +447,7 @@ namespace pointed
   definition eq_of_phomotopy (p : k ~* l) : k = l :=
   to_inv (ppi_eq_equiv k l) p
 
-  definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) :
+  definition eq_of_phomotopy_refl (k : ppi P p₀) : eq_of_phomotopy (phomotopy.refl k) = idpath k :=
-    eq_of_phomotopy (phomotopy.refl f) = idpath f :=
   begin
     apply to_inv_eq_of_eq, reflexivity
   end
@@ -480,11 +479,17 @@ namespace pointed
     induction t, exact phomotopy_of_eq_idp k ▸ q,
   end
 
+  definition phomotopy_rec_idp' (Q : Π ⦃k' : ppi P p₀⦄, (k ~* k') → (k = k') → Type)
+    (q : Q phomotopy.rfl idp) ⦃k' : ppi P p₀⦄ (H : k ~* k') : Q H (eq_of_phomotopy H) :=
+  begin
+    induction H using phomotopy_rec_idp,
+    exact transport (Q phomotopy.rfl) !eq_of_phomotopy_refl⁻¹ q
+  end
+
   attribute phomotopy.rec' [recursor]
 
-  definition phomotopy_rec_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B}
+  definition phomotopy_rec_eq_phomotopy_of_eq {Q : (k ~* l) → Type} (p : k = l)
-    {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) :
+    (H : Π(q : k = l), Q (phomotopy_of_eq q)) : phomotopy_rec_eq (phomotopy_of_eq p) H = H p :=
-    phomotopy_rec_eq (phomotopy_of_eq p) H = H p :=
   begin
     unfold phomotopy_rec_eq,
     refine ap (λp, p ▸ _) !adj ⬝ _,
@@ -492,11 +497,33 @@ namespace pointed
     apply apdt
   end
 
-  definition phomotopy_rec_idp_refl {A B : Type*} (f : A →* B)
+  definition phomotopy_rec_idp_refl {Q : Π{l}, (k ~* l) → Type} (H : Q (phomotopy.refl k)) :
-    {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) :
     phomotopy_rec_idp phomotopy.rfl H = H :=
   !phomotopy_rec_eq_phomotopy_of_eq
 
+  definition phomotopy_rec_idp'_refl (Q : Π ⦃k' : ppi P p₀⦄, (k ~* k') → (k = k') → Type)
+    (q : Q phomotopy.rfl idp) :
+    phomotopy_rec_idp' Q q phomotopy.rfl = transport (Q phomotopy.rfl) !eq_of_phomotopy_refl⁻¹ q :=
+  !phomotopy_rec_idp_refl
+
+  /- maps out of or into contractible types -/
+  definition phomotopy_of_is_contr_cod [constructor] (k l : ppi P p₀) [Πa, is_contr (P a)] :
+    k ~* l :=
+  phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr
+
+  definition phomotopy_of_is_contr_cod_pmap [constructor] (f g : A →* B) [is_contr B] : f ~* g :=
+  phomotopy_of_is_contr_cod f g
+
+  definition phomotopy_of_is_contr_dom [constructor] (k l : ppi P p₀) [is_contr A] : k ~* l :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, exact eq_of_pathover_idp (change_path !is_prop.elim
+      (apd k !is_prop.elim ⬝op respect_pt k ⬝ (respect_pt l)⁻¹ ⬝o apd l !is_prop.elim)) },
+    rewrite [▸*, +is_prop_elim_self, +apd_idp, cono_idpo],
+    refine ap (λx, eq_of_pathover_idp (change_path x _)) !is_prop_elim_self ◾ idp ⬝ _,
+    xrewrite [change_path_idp, idpo_concato_eq, inv_con_cancel_right],
+  end
+
   /- adjunction between (-)₊ : Type → Type* and pType.carrier : Type* → Type  -/
   definition pmap_equiv_left (A : Type) (B : Type*) : A₊ →* B ≃ (A → B) :=
   begin

hott/types/pointed2.hlean

@@ -18,7 +18,7 @@ import algebra.homotopy_group eq2
 open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function bool
 
 namespace pointed
-  variables {A B C : Type*}
+  variables {A B C : Type*} {P : A → Type} {p₀ : P pt} {k k' l m n : ppi P p₀}
 
   section psquare
   /-
@@ -134,14 +134,35 @@ namespace pointed
 
   definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) :
     f ~* pconst punit A :=
+  !phomotopy_of_is_contr_dom
+
+  definition punit_ppi [constructor] (P : punit → Type*) (p₀ : P ⋆) : ppi P p₀ :=
   begin
-    fapply phomotopy.mk,
+    fapply ppi.mk, intro u, induction u, exact p₀,
-    { intro u, induction u, exact respect_pt f },
+    reflexivity
-    { reflexivity }
   end
 
+  definition punit_ppi_phomotopy [constructor] {P : punit → Type*} {p₀ : P ⋆} (f : ppi P p₀) :
+    f ~* punit_ppi P p₀ :=
+  !phomotopy_of_is_contr_dom
+
+  definition is_contr_punit_ppi (P : punit → Type*) (p₀ : P ⋆) : is_contr (ppi P p₀) :=
+  is_contr.mk (punit_ppi P p₀) (λf, eq_of_phomotopy (punit_ppi_phomotopy f)⁻¹*)
+
   definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) :=
-  is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*)
+  !is_contr_punit_ppi
+
+  -- definition phomotopy_eq_equiv (h₁ h₂ : k ~* l) :
+  --   (h₁ = h₂) ≃ Σ(p : to_homotopy h₁ ~ to_homotopy h₂),
+  --     whisker_right (respect_pt l) (p pt) ⬝ to_homotopy_pt h₂ = to_homotopy_pt h₁ :=
+  -- begin
+  --   refine !ppi_eq_equiv ⬝e !phomotopy.sigma_char ⬝e sigma_equiv_sigma_right _,
+  --   intro p,
+  -- end
+
+  /- Short term TODO: generalize to dependent maps (use ppi_eq_equiv?)
+     Long term TODO: use homotopies between pointed homotopies, not equalities
+  -/
 
   definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) :
     (h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k),
@@ -173,12 +194,11 @@ namespace pointed
     (q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k :=
   phomotopy_eq p (eq_of_square q)⁻¹
 
-  definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p :=
+  definition trans_refl (p : k ~* l) : p ⬝* phomotopy.rfl = p :=
   begin
-    induction A with A a₀, induction B with B b₀,
+    induction A with A a₀,
-    induction f with f f₀, induction g with g g₀, induction p with p p₀,
+    induction k with k k₀, induction l with l l₀, induction p with p p₀', esimp at * ⊢,
-    esimp at *, induction g₀, induction p₀,
+    induction l₀, induction p₀', reflexivity,
-    reflexivity
   end
 
   definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) :
@@ -188,77 +208,66 @@ namespace pointed
     exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹
   end
 
-  definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p :=
+  definition refl_trans (p : k ~* l) : phomotopy.rfl ⬝* p = p :=
   begin
     induction p using phomotopy_rec_idp,
-    induction A with A a₀, induction B with B b₀,
+    apply trans_refl
-    induction f with f f₀, esimp at *, induction f₀,
-    reflexivity
   end
 
-  definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h)
+  definition trans_assoc (p : k ~* l) (q : l ~* m) (r : m ~* n) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) :=
-    (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) :=
   begin
     induction r using phomotopy_rec_idp,
     induction q using phomotopy_rec_idp,
     induction p using phomotopy_rec_idp,
-    induction B with B b₀,
+    induction k with k k₀, induction k₀,
-    induction f with f f₀, esimp at *, induction f₀,
     reflexivity
   end
 
-  definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f :=
+  definition refl_symm : phomotopy.rfl⁻¹* = phomotopy.refl k :=
   begin
-    induction B with B b₀,
+    induction k with k k₀, induction k₀,
-    induction f with f f₀, esimp at *, induction f₀,
     reflexivity
   end
 
-  definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p :=
+  definition symm_symm (p : k ~* l) : p⁻¹*⁻¹* = p :=
-  phomotopy_eq (λa, !inv_inv)
+  begin
-    begin
+    induction p using phomotopy_rec_idp, induction k with k k₀, induction k₀, reflexivity
-      induction p using phomotopy_rec_idp, induction f with f f₀, induction B with B b₀,
+  end
-      esimp at *, induction f₀, reflexivity
-    end
 
-  definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl :=
+  definition trans_right_inv (p : k ~* l) : p ⬝* p⁻¹* = phomotopy.rfl :=
   begin
     induction p using phomotopy_rec_idp, exact !refl_trans ⬝ !refl_symm
   end
 
-  definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl :=
+  definition trans_left_inv (p : k ~* l) : p⁻¹* ⬝* p = phomotopy.rfl :=
   begin
     induction p using phomotopy_rec_idp, exact !trans_refl ⬝ !refl_symm
   end
 
-  definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h}
+  definition trans2 {p p' : k ~* l} {q q' : l ~* m} (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' :=
-    (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' :=
   ap011 phomotopy.trans r s
 
   definition pcompose3 {A B C : Type*} {g g' : B →* C} {f f' : A →* B}
   {p p' : g ~* g'} {q q' : f ~* f'} (r : p = p') (s : q = q') : p ◾* q = p' ◾* q' :=
   ap011 pcompose2 r s
 
-  definition symm2 {A B : Type*} {f g : A →* B} {p p' : f ~* g} (r : p = p') : p⁻¹* = p'⁻¹* :=
+  definition symm2 {p p' : k ~* l} (r : p = p') : p⁻¹* = p'⁻¹* :=
   ap phomotopy.symm r
 
   infixl ` ◾** `:80 := pointed.trans2
   infixl ` ◽* `:81 := pointed.pcompose3
   postfix `⁻²**`:(max+1) := pointed.symm2
 
-  definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) :
+  definition trans_symm (p : k ~* l) (q : l ~* m) : (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* :=
-    (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* :=
   begin
     induction p using phomotopy_rec_idp, induction q using phomotopy_rec_idp,
     exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹
   end
 
-  definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h}
+  definition phwhisker_left (p : k ~* l) {q q' : l ~* m} (s : q = q') : p ⬝* q = p ⬝* q' :=
-    (s : q = q') : p ⬝* q = p ⬝* q' :=
   idp ◾** s
 
-  definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h)
+  definition phwhisker_right {p p' : k ~* l} (q : l ~* m) (r : p = p') : p ⬝* q = p' ⬝* q :=
-    (r : p = p') : p ⬝* q = p' ⬝* q :=
   r ◾** idp
 
   definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) :
@@ -325,36 +334,36 @@ namespace pointed
     refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹
   end
 
-  definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition trans_eq_of_eq_symm_trans {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : q = p⁻¹* ⬝* r) :
-    {r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r :=
+    p ⬝* q = r :=
   idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_right_inv p ◾** idp ⬝ !refl_trans
 
-  definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition eq_symm_trans_of_trans_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p ⬝* q = r) :
-    {r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r :=
+    q = p⁻¹* ⬝* r :=
   !refl_trans⁻¹ ⬝ !trans_left_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s
 
-  definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition trans_eq_of_eq_trans_symm {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p = r ⬝* q⁻¹*) :
-    {r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r :=
+    p ⬝* q = r :=
   s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_left_inv q ⬝ !trans_refl
 
-  definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition eq_trans_symm_of_trans_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p ⬝* q = r) :
-    {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* :=
+    p = r ⬝* q⁻¹* :=
   !trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
 
-  definition eq_trans_of_symm_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition eq_trans_of_symm_trans_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p⁻¹* ⬝* r = q) :
-    {r : f ~* h} (s : p⁻¹* ⬝* r = q) : r = p ⬝* q :=
+    r = p ⬝* q :=
   !refl_trans⁻¹ ⬝ !trans_right_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s
 
-  definition symm_trans_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition symm_trans_eq_of_eq_trans {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : r = p ⬝* q) :
-    {r : f ~* h} (s : r = p ⬝* q) : p⁻¹* ⬝* r = q :=
+    p⁻¹* ⬝* r = q :=
   idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_left_inv p ◾** idp ⬝ !refl_trans
 
-  definition eq_trans_of_trans_symm_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition eq_trans_of_trans_symm_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : r ⬝* q⁻¹* = p) :
-    {r : f ~* h} (s : r ⬝* q⁻¹* = p) : r = p ⬝* q :=
+    r = p ⬝* q :=
   !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
 
-  definition trans_symm_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
+  definition trans_symm_eq_of_eq_trans {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : r = p ⬝* q) :
-    {r : f ~* h} (s : r = p ⬝* q) : r ⬝* q⁻¹* = p :=
+    r ⬝* q⁻¹* = p :=
   s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_right_inv q ⬝ !trans_refl
 
   section phsquare
@@ -362,7 +371,7 @@ namespace pointed
     Squares of pointed homotopies
   -/
 
-  variables {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B}
+  variables {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : ppi P p₀}
             {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀}
             {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂}
             {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂}
@@ -495,6 +504,13 @@ namespace pointed
           !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹
   end
 
+  end phsquare
+
+  section nondep_phsquare
+
+  variables {f f' f₀₀ f₂₀ f₀₂ f₂₂ : A →* B}
+            {p₁₀ : f₀₀ ~* f₂₀} {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₁₂ : f₀₂ ~* f₂₂}
+
   definition pwhisker_left_phsquare (f : B →* C) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
     phsquare (pwhisker_left f p₁₀) (pwhisker_left f p₁₂)
              (pwhisker_left f p₀₁) (pwhisker_left f p₂₁) :=
@@ -505,9 +521,9 @@ namespace pointed
              (pwhisker_right f p₀₁) (pwhisker_right f p₂₁) :=
   !pwhisker_right_trans⁻¹ ⬝ ap (pwhisker_right f) p ⬝ !pwhisker_right_trans
 
-  end phsquare
+  end nondep_phsquare
 
-  definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) :
+  definition phomotopy_of_eq_con (p : k = l) (q : l = m) :
     phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q :=
   begin induction q, induction p, exact !trans_refl⁻¹ end
 

hott/types/unit.hlean

@@ -32,6 +32,9 @@ namespace unit
 
   notation `unit*` := punit
 
+  definition is_contr_punit [instance] : is_contr punit :=
+  is_contr_unit
+
   definition unit_arrow_eq {X : Type} (f : unit → X) : (λx, f ⋆) = f :=
   by apply eq_of_homotopy; intro u; induction u; reflexivity