Finish the naturality of the smash-pmap adjunction

algebra/product_group.hlean

@@ -59,5 +59,6 @@ namespace group
   AbGroup.mk _ (ab_group_prod G G')
 
   infix ` ×g `:30 := group.product
+  infix ` ×ag `:30 := group.ab_product
 
 end group

choice.hlean

@@ -64,9 +64,9 @@ end
 definition has_choice_bool [instance] (n : ℕ₋₂) : has_choice n bool :=
 has_choice_equiv_closed n bool_equiv_unit_sum_unit _
 
-definition has_choice_lift [instance] (n : ℕ₋₂) (A : Type) [has_choice n A] :
+definition has_choice_lift.{u v} [instance] (n : ℕ₋₂) (A : Type) [has_choice n A] :
-  has_choice n (lift A) :=
+  has_choice n (lift.{u v} A) :=
-has_choice_equiv_closed n !equiv_lift⁻¹ᵉ _
+sorry --has_choice_equiv_closed n !equiv_lift⁻¹ᵉ _
 
 definition has_choice_punit [instance] (n : ℕ₋₂) : has_choice n punit := has_choice_unit n
 definition has_choice_pbool [instance] (n : ℕ₋₂) : has_choice n pbool := has_choice_bool n

homotopy/cohomology.hlean

@@ -6,36 +6,36 @@ Authors: Floris van Doorn
 Reduced cohomology of spectra and cohomology theories
 -/
 
-import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib
+import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib ..algebra.product_group
 
 open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
-     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit
+     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi
 
 -- TODO: move
-structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
   ( im_in_ker : Π(a:A), g (f a) = pt)
   ( ker_in_im : Π(b:B), (g b = pt) → image f b)
 
-definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
+definition is_short_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
-is_exact f g
+is_short_exact f g
 
-definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
+definition is_short_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
-  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
+  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_short_exact_g f g :=
-is_exact.mk H₁ H₂
+is_short_exact.mk H₁ H₂
 
-definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
+definition is_short_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
-  (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
+  (H : is_short_exact_t f g) : @is_short_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
 begin
   constructor,
   { intro a, esimp, induction a with a,
-    exact ap tr (is_exact_t.im_in_ker H a) },
+    exact ap tr (is_short_exact_t.im_in_ker H a) },
   { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q,
-    induction is_exact_t.ker_in_im H b q with a r,
+    induction is_short_exact_t.ker_in_im H b q with a r,
     exact image.mk (tr a) (ap tr r) }
 end
 
-definition is_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C}
+definition is_short_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C}
-  (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' :=
+  (p : f ~ f') (q : g ~ g') (H : is_short_exact f g) : is_short_exact f' g' :=
 begin
   induction p using homotopy.rec_on_idp,
   induction q using homotopy.rec_on_idp,
@@ -199,8 +199,8 @@ end
 /- exactness -/
 
 definition cohomology_exact {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
-  is_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) :=
+  is_short_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) :=
-is_exact_trunc_functor (cofiber_exact f)
+is_short_exact_trunc_functor (cofiber_exact f)
 
 /- additivity -/
 
@@ -253,7 +253,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
   (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
   (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
     Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y)
-  (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f))
+  (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_short_exact_g (Hh n (pcod f)) (Hh n f))
   (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
     is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
 
@@ -264,6 +264,9 @@ attribute cohomology_theory.HH [coercion]
 postfix `^→`:90 := cohomology_theory.Hh
 open cohomology_theory
 
+definition Hequiv (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X ≃* Y) : H n Y ≃ H n X :=
+equiv_of_isomorphism (Hiso H n f)
+
 definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (psusp X) ≃g H (pred n) X :=
 isomorphism_of_eq (ap (λn, H n _) proof (sub_add_cancel n 1)⁻¹ qed) ⬝g cohomology_theory.Hsusp H (pred n) X
 
@@ -279,23 +282,41 @@ definition Hsusp_neg_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*}
   H ^→ n (psusp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f :=
 sorry
 
-definition Hadditive0 (H : cohomology_theory) (n : ℤ) :
+definition Hadditive_equiv (H : cohomology_theory) (n : ℤ) {I : Type} (X : I → Type*) (H2 : has_choice 0 I)
+  : H n (⋁ X) ≃g Πᵍ i, H n (X i) :=
+isomorphism.mk _ (Hadditive H n X H2)
+
+definition Hlift_empty.{u} (H : cohomology_theory.{u}) (n : ℤ) :
   is_contr (H n (plift punit)) :=
 let P : lift empty → Type* := lift.rec empty.elim in
 let x := Hadditive H n P _ in
 begin
   note z := equiv.mk _ x,
   refine @(is_trunc_equiv_closed_rev -2 (_ ⬝e z ⬝e _)) !is_contr_unit,
-  repeat exact sorry
+    refine Hequiv H n (pequiv_punit_of_is_contr _ _ ⬝e* !pequiv_plift),
---  refine equiv_of_isomorphism (Hiso H n (_ ⬝e* _)),
+    apply is_contr_fwedge_of_neg, intro y, induction y with y, exact y,
+  apply equiv_unit_of_is_contr, apply is_contr_pi_of_neg, intro y, induction y with y, exact y
 end
 
+definition Hempty (H : cohomology_theory.{0}) (n : ℤ) :
+  is_contr (H n punit) :=
+@(is_trunc_equiv_closed _ (Hequiv H n !pequiv_plift)) (Hlift_empty H n)
+
 definition Hconst (H : cohomology_theory) (n : ℤ) {X Y : Type*} (y : H n Y) : H ^→ n (pconst X Y) y = 1 :=
 begin
-  refine !one_mul⁻¹ ⬝ _, exact sorry
+  refine Hhomotopy H n (pconst_pcompose (pconst X (plift punit)))⁻¹* y ⬝ _,
+  refine Hcompose H n _ _ y ⬝ _,
+  refine ap (H ^→ n _) (@eq_of_is_contr _ (Hlift_empty H n) _ 1) ⬝ _,
+  apply respect_one
 end
 
-definition cohomology_theory_spectrum [constructor] (Y : spectrum) : cohomology_theory :=
+-- definition Hwedge (H : cohomology_theory) (n : ℤ) (A B : Type*) : H n (A ∨ B) ≃g H n A ×ag H n B :=
+-- begin
+--   refine Hiso H n (pwedge_pequiv_fwedge A B)⁻¹ᵉ* ⬝g _,
+--   refine Hadditive_equiv H n _ _ ⬝g _
+-- end
+
+definition cohomology_theory_spectrum.{u} [constructor] (Y : spectrum.{u}) : cohomology_theory.{u} :=
 cohomology_theory.mk
   (λn A, H^n[A, Y])
   (λn A B f, cohomology_isomorphism f Y n)
@@ -310,6 +331,13 @@ cohomology_theory.mk
   (λn A B f, cohomology_exact f Y n)
   (λn I A H, spectrum_additive H A Y n)
 
+-- set_option pp.universes true
+-- set_option pp.abbreviations false
+-- print cohomology_theory_spectrum
+-- print EM_spectrum
+-- print has_choice_lift
+-- print equiv_lift
+-- print has_choice_equiv_closed
 definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
 ⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
 

homotopy/fwedge.hlean

@@ -86,11 +86,14 @@ namespace fwedge
     { exact glue ff }
   end
 
-  definition is_contr_fwedge_empty : is_contr (⋁(empty.rec _)) :=
+  definition is_contr_fwedge_of_neg {I : Type} (P : I → Type*) (H : ¬ I) : is_contr (⋁P) :=
   begin
     apply is_contr.mk pt, intro x, induction x, contradiction, reflexivity, contradiction
   end
 
+  definition is_contr_fwedge_empty [instance] : is_contr (⋁empty.elim) :=
+  is_contr_fwedge_of_neg _ id
+
   definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X :=
   begin
     fconstructor,
@@ -132,6 +135,6 @@ namespace fwedge
 
   definition trunc_fwedge_pmap_equiv.{u} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I)
     (F : I → pType.{u}) (X : pType.{u}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) :=
-  trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv H (λi, F i →* X)
+  trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv (λi, F i →* X)
 
 end fwedge

homotopy/pushout.hlean

@@ -464,7 +464,7 @@ namespace pushout
 
   /- universal property of cofiber -/
 
-  structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
   ( im_in_ker : Π(a:A), g (f a) = pt)
   ( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
 
@@ -491,7 +491,7 @@ namespace pushout
   end
 
   definition cofiber_exact {X Y Z : Type*} (f : X →* Y) :
-    is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) :=
+    is_short_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) :=
   begin
     constructor,
     { intro g, apply eq_of_phomotopy, apply cofiber_exact_1 },

homotopy/smash.hlean

@@ -9,14 +9,51 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w
 
   /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/
 
-  /- To prove: associative, A ∧ S¹ ≃ ΣA -/
+  /- To prove: A ∧ S¹ ≃ ΣA -/
 
+  /- associativity is mostly proven in smash_adjoint, the only hole in the proof is in this file -/
 variables {A B C D E F : Type*}
 
 namespace smash
 
   open pushout
 
+  protected definition rec_eq {A B : Type*} {C : Type} {f g : smash A B → C}
+    (Pmk : Πa b, f (smash.mk a b) = g (smash.mk a b))
+    (Pl : f auxl = g auxl) (Pr : f auxr = g auxr)
+    (Pgl : Πa, square (Pmk a pt) Pl (ap f (gluel a)) (ap g (gluel a)))
+    (Pgr : Πb, square (Pmk pt b) Pr (ap f (gluer b)) (ap g (gluer b))) (x : smash' A B) : f x = g x :=
+  begin
+    induction x with a b a b,
+    { exact Pmk a b },
+    { exact Pl },
+    { exact Pr },
+    { apply eq_pathover, apply Pgl },
+    { apply eq_pathover, apply Pgr }
+  end
+
+  definition rec_eq_gluel {A B : Type*} {C : Type} {f g : smash A B → C}
+    {Pmk : Πa b, f (smash.mk a b) = g (smash.mk a b)}
+    {Pl : f auxl = g auxl} {Pr : f auxr = g auxr}
+    (Pgl : Πa, square (Pmk a pt) Pl (ap f (gluel a)) (ap g (gluel a)))
+    (Pgr : Πb, square (Pmk pt b) Pr (ap f (gluer b)) (ap g (gluer b))) (a : A) :
+      natural_square (smash.rec_eq Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a :=
+  begin
+    refine ap square_of_pathover !rec_gluel ⬝ _,
+    apply to_right_inv !eq_pathover_equiv_square
+  end
+
+  definition rec_eq_gluer {A B : Type*} {C : Type} {f g : smash A B → C}
+    {Pmk : Πa b, f (smash.mk a b) = g (smash.mk a b)}
+    {Pl : f auxl = g auxl} {Pr : f auxr = g auxr}
+    (Pgl : Πa, square (Pmk a pt) Pl (ap f (gluel a)) (ap g (gluel a)))
+    (Pgr : Πb, square (Pmk pt b) Pr (ap f (gluer b)) (ap g (gluer b))) (b : B) :
+      natural_square (smash.rec_eq Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b :=
+  begin
+    refine ap square_of_pathover !rec_gluer ⬝ _,
+    apply to_right_inv !eq_pathover_equiv_square
+  end
+
   definition smash_functor' [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D :=
   begin
     fapply pushout.functor,
@@ -50,6 +87,18 @@ namespace smash
     induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity
   end
 
+  definition functor_gluel2 {C D : Type} (f : A → C) (g : B → D) (a : A) :
+    ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluel a) = gluel (f a) :=
+  begin
+    refine !pushout.elim_glue ⬝ !idp_con
+  end
+
+  definition functor_gluer2 {C D : Type} (f : A → C) (g : B → D) (b : B) :
+    ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluer b) = gluer (g b) :=
+  begin
+    refine !pushout.elim_glue ⬝ !idp_con
+  end
+
   definition functor_gluel' (f : A →* C) (g : B →* D) (a a' : A) :
     ap (smash_functor f g) (gluel' a a') = ap (smash.mk (f a)) (respect_pt g) ⬝
       gluel' (f a) (f a') ⬝ (ap (smash.mk (f a')) (respect_pt g))⁻¹ :=
@@ -73,23 +122,31 @@ namespace smash
 
   /- the statements of the above rules becomes easier if one of the functions respects the basepoint
      by reflexivity -/
-  definition functor_gluel'2 {D : Type} (f : A →* C) (g : B → D) (a a' : A) :
+  -- definition functor_gluel'2 {D : Type} (f : A →* C) (g : B → D) (a a' : A) :
-    ap (smash_functor f (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') :=
+  --   ap (smash_functor f (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') :=
-  begin
+  -- begin
-    refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _,
+  --   refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _,
-    refine (!functor_gluel ⬝ !idp_con) ◾  (!functor_gluel ⬝ !idp_con)⁻²
+  --   refine (!functor_gluel ⬝ !idp_con) ◾  (!functor_gluel ⬝ !idp_con)⁻²
-  end
+  -- end
 
-  definition functor_gluer'2 {C : Type} (f : A → C) (g : B →* D) (b b' : B) :
+  -- definition functor_gluer'2 {C : Type} (f : A → C) (g : B →* D) (b b' : B) :
-    ap (smash_functor (pmap_of_map f pt) g) (gluer' b b') = gluer' (g b) (g b') :=
+  --   ap (smash_functor (pmap_of_map f pt) g) (gluer' b b') = gluer' (g b) (g b') :=
-  begin
+  -- begin
-    refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _,
+  --   refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _,
-    refine (!functor_gluer ⬝ !idp_con) ◾  (!functor_gluer ⬝ !idp_con)⁻²
+  --   refine (!functor_gluer ⬝ !idp_con) ◾  (!functor_gluer ⬝ !idp_con)⁻²
-  end
+  -- end
 
-  lemma functor_gluel'2_same {D : Type} (f : A →* C) (g : B → D) (a : A) :
+  definition functor_gluel'2 {C D : Type} (f : A → C) (g : B → D) (a a' : A) :
+    ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') :=
+  !ap_con ⬝ whisker_left _ !ap_inv ⬝ !functor_gluel2 ◾ !functor_gluel2⁻²
+
+  definition functor_gluer'2 {C D : Type} (f : A → C) (g : B → D) (b b' : B) :
+    ap (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (gluer' b b') = gluer' (g b) (g b') :=
+  !ap_con ⬝ whisker_left _ !ap_inv ⬝ !functor_gluer2 ◾ !functor_gluer2⁻²
+
+  lemma functor_gluel'2_same {C D : Type} (f : A → C) (g : B → D) (a : A) :
     functor_gluel'2 f (pmap_of_map g pt) a a =
-    ap02 (smash_functor f (pmap_of_map g pt)) (con.right_inv (gluel a)) ⬝
+    ap02 (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (con.right_inv (gluel a)) ⬝
     (con.right_inv (gluel (f a)))⁻¹ :=
   begin
     refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹,
@@ -100,9 +157,9 @@ namespace smash
     apply con_right_inv_natural
   end
 
-  lemma functor_gluer'2_same {C : Type} (f : A → C) (g : B →* D) (b : B) :
+  lemma functor_gluer'2_same {C D : Type} (f : A → C) (g : B → D) (b : B) :
     functor_gluer'2 (pmap_of_map f pt) g b b =
-    ap02 (smash_functor (pmap_of_map f pt) g) (con.right_inv (gluer b)) ⬝
+    ap02 (smash_functor (pmap_of_map f pt) (pmap_of_map g pt)) (con.right_inv (gluer b)) ⬝
     (con.right_inv (gluer (g b)))⁻¹ :=
   begin
     refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹,
@@ -113,56 +170,108 @@ namespace smash
     apply con_right_inv_natural
   end
 
-  definition smash_functor_pcompose_homotopy (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) :
+  -- definition smash_functor_pcompose_homotopy [unfold 11] (f' : C →* E) (f : A →* C) (g' : D →* F)
-    smash_functor (f' ∘* f) (g' ∘* g) ~ smash_functor f' g' ∘* smash_functor f g :=
+  --   (g : B →* D) : smash_functor (f' ∘* f) (g' ∘* g) ~ smash_functor f' g' ∘* smash_functor f g :=
+  -- begin
+  --   intro x, induction x with a b a b,
+  --   { reflexivity },
+  --   { reflexivity },
+  --   { reflexivity },
+  --   { apply eq_pathover, exact abstract begin apply hdeg_square,
+  --     refine !functor_gluel ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹,
+  --     refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluel⁻¹,
+  --     refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluel⁻¹ qed ⬝ !ap_con⁻¹ end end },
+  --   { apply eq_pathover, exact abstract begin apply hdeg_square,
+  --     refine !functor_gluer ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹,
+  --     refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluer⁻¹,
+  --     refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluer⁻¹ qed ⬝ !ap_con⁻¹ end end }
+  -- end
+
+  -- definition smash_functor_pcompose [constructor] (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) :
+  --   smash_functor (f' ∘* f) (g' ∘* g) ~* smash_functor f' g' ∘* smash_functor f g :=
+  -- begin
+  --   fapply phomotopy.mk,
+  --   { exact smash_functor_pcompose_homotopy f' f g' g },
+  --   { exact abstract begin induction C, induction D, induction E, induction F,
+  --     induction f with f f₀, induction f' with f' f'₀, induction g with g g₀,
+  --     induction g' with g' g'₀, esimp at *,
+  --     induction f₀, induction f'₀, induction g₀, induction g'₀, reflexivity end end }
+  -- end
+
+  definition smash_functor_pcompose_homotopy [unfold 11] {C D E F : Type}
+    (f' : C → E) (f : A → C) (g' : D → F) (g : B → D) :
+    smash_functor (pmap_of_map f' (f pt) ∘* pmap_of_map f pt)
+                  (pmap_of_map g' (g pt) ∘* pmap_of_map g pt) ~
+    smash_functor (pmap_of_map f' (f pt)) (pmap_of_map g' (g pt)) ∘*
+    smash_functor (pmap_of_map f pt) (pmap_of_map g pt) :=
   begin
     intro x, induction x with a b a b,
     { reflexivity },
     { reflexivity },
     { reflexivity },
-    { apply eq_pathover, apply hdeg_square,
+    { apply eq_pathover, refine !functor_gluel2 ⬝ph _, esimp,
-      refine !functor_gluel ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹,
+      refine _ ⬝hp (ap_compose (smash_functor _ _) _ _)⁻¹,
-      refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluel⁻¹,
+      refine _ ⬝hp ap02 _ !functor_gluel2⁻¹, refine _ ⬝hp !functor_gluel2⁻¹, exact hrfl },
-      refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluel⁻¹ qed ⬝ !ap_con⁻¹, },
+    { apply eq_pathover, refine !functor_gluer2 ⬝ph _, esimp,
-    { apply eq_pathover, apply hdeg_square,
+      refine _ ⬝hp (ap_compose (smash_functor _ _) _ _)⁻¹,
-      refine !functor_gluer ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹,
+      refine _ ⬝hp ap02 _ !functor_gluer2⁻¹, refine _ ⬝hp !functor_gluer2⁻¹, exact hrfl }
-      refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluer⁻¹,
-      refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluer⁻¹ qed ⬝ !ap_con⁻¹, }
   end
 
-  definition smash_functor_pcompose [constructor] (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) :
+  definition smash_functor_pcompose (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) :
     smash_functor (f' ∘* f) (g' ∘* g) ~* smash_functor f' g' ∘* smash_functor f g :=
   begin
+    induction C with C, induction D with D, induction E with E, induction F with F,
+    induction f with f f₀, induction f' with f' f'₀, induction g with g g₀,
+    induction g' with g' g'₀, esimp at *,
+    induction f₀, induction f'₀, induction g₀, induction g'₀,
     fapply phomotopy.mk,
-    { exact smash_functor_pcompose_homotopy f' f g' g },
+    { rexact smash_functor_pcompose_homotopy f' f g' g },
-    { exact abstract begin induction C, induction D, induction E, induction F,
+    { reflexivity }
-      induction f with f f₀, induction f' with f' f'₀, induction g with g g₀, induction g' with g' g'₀,
-      esimp at *, induction f₀, induction f'₀, induction g₀, induction g'₀, reflexivity end end }
   end
 
+  -- definition smash_functor_homotopy [unfold 11] {f f' : A →* C} {g g' : B →* D}
+  --   (h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~ smash_functor f' g' :=
+  -- begin
+  --   intro x, induction x with a b a b,
+  --   { exact ap011 smash.mk (h₁ a) (h₂ b) },
+  --   { reflexivity },
+  --   { reflexivity },
+  --   { apply eq_pathover,
+  --     refine !functor_gluel ⬝ph _ ⬝hp !functor_gluel⁻¹,
+  --     refine _ ⬝v square_of_eq_top (ap_mk_left (h₁ a)),
+  --     exact ap011_ap_square_right smash.mk (h₁ a) (to_homotopy_pt h₂) },
+  --   { apply eq_pathover,
+  --     refine !functor_gluer ⬝ph _ ⬝hp !functor_gluer⁻¹,
+  --     refine _ ⬝v square_of_eq_top (ap_mk_right (h₂ b)),
+  --     exact ap011_ap_square_left smash.mk (h₂ b) (to_homotopy_pt h₁) },
+  -- end
+
+  -- definition smash_functor_phomotopy [constructor] {f f' : A →* C} {g g' : B →* D}
+  --   (h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~* smash_functor f' g' :=
+  -- begin
+  --   apply phomotopy.mk (smash_functor_homotopy h₁ h₂),
+  --   induction h₁ with h₁ h₁₀, induction h₂ with h₂ h₂₀,
+  --   induction f with f f₀, induction g with g g₀,
+  --   induction f' with f' f'₀, induction g' with g' g'₀,
+  --   induction C with C c₀, induction D with D d₀, esimp at *,
+  --   induction h₁₀, induction h₂₀, induction f'₀, induction g'₀,
+  --   exact !ap_ap011⁻¹
+  -- end
+
   definition smash_functor_phomotopy [constructor] {f f' : A →* C} {g g' : B →* D}
     (h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~* smash_functor f' g' :=
   begin
     induction h₁ using phomotopy_rec_on_idp,
     induction h₂ using phomotopy_rec_on_idp,
     reflexivity
-    -- fapply phomotopy.mk,
-    -- { intro x, induction x with a b a b,
-    --   { exact ap011 smash.mk (h₁ a) (h₂ b) },
-    --   { reflexivity },
-    --   { reflexivity },
-    --   { apply eq_pathover,
-    --     refine !functor_gluel ⬝ph _ ⬝hp !functor_gluel⁻¹, exact sorry },
-    --   { apply eq_pathover,
-    --     refine !functor_gluer ⬝ph _ ⬝hp !functor_gluer⁻¹, exact sorry }},
-    -- { esimp, }
   end
 
   definition smash_functor_phomotopy_refl [constructor] (f : A →* C) (g : B →* D) :
     smash_functor_phomotopy (phomotopy.refl f) (phomotopy.refl g) = phomotopy.rfl :=
   !phomotopy_rec_on_idp_refl ⬝ !phomotopy_rec_on_idp_refl
 
-  definition smash_functor_pid [constructor] (A B : Type*) : smash_functor (pid A) (pid B) ~* pid (A ∧ B) :=
+  definition smash_functor_pid [constructor] (A B : Type*) :
+    smash_functor (pid A) (pid B) ~* pid (A ∧ B) :=
   begin
     fapply phomotopy.mk,
     { intro x, induction x with a b a b,
@@ -182,26 +291,133 @@ namespace smash
     : smash_functor (f' ∘* f) (pid B) ~* smash_functor f' (pid B) ∘* smash_functor f (pid B) :=
   smash_functor_phomotopy phomotopy.rfl !pid_pcompose⁻¹* ⬝* !smash_functor_pcompose
 
-  definition smash_functor_pconst_right_homotopy [unfold 6] (f : A →* C) (x : A ∧ B) :
+  -- definition smash_functor_pconst_right_homotopy [unfold 6] (f : A →* C) (x : A ∧ B) :
-    smash_functor f (pconst B D) x = pt :=
+  --   smash_functor f (pconst B D) x = pt :=
+  -- begin
+  --   induction x with a b a b,
+  --   { exact gluel' (f a) pt },
+  --   { exact (gluel pt)⁻¹ },
+  --   { exact (gluer pt)⁻¹ },
+  --   { apply eq_pathover, refine !functor_gluel ⬝ !idp_con ⬝ph _ ⬝hp !ap_constant⁻¹,
+  --     apply square_of_eq, reflexivity },
+  --   { apply eq_pathover, refine !functor_gluer ⬝ph _ ⬝hp !ap_constant⁻¹,
+  --     apply whisker_lb, apply square_of_eq, exact !ap_mk_left⁻¹ }
+  -- end
+
+  -- definition smash_functor_pconst_right [constructor] (f : A →* C) :
+  --   smash_functor f (pconst B D) ~* pconst (A ∧ B) (C ∧ D) :=
+  -- begin
+  --   fapply phomotopy.mk,
+  --   { exact smash_functor_pconst_right_homotopy f },
+  --   { refine (ap_mk_left (respect_pt f))⁻¹ ⬝ _,
+  --     induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity }
+  -- end
+
+--  set_option pp.all true
+  definition smash_functor_pconst_right_homotopy [unfold 6] {C : Type} (f : A → C) (x : A ∧ B) :
+    smash_functor (pmap_of_map f pt) (pconst B D) x = pt :=
   begin
     induction x with a b a b,
     { exact gluel' (f a) pt },
     { exact (gluel pt)⁻¹ },
     { exact (gluer pt)⁻¹ },
-    { apply eq_pathover_constant_right, refine !functor_gluel ⬝ !idp_con ⬝ph _,
+    { apply eq_pathover, note x := functor_gluel2 f (λx : B, Point D) a, esimp [pconst] at *,
-      apply square_of_eq, reflexivity },
+      refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq, reflexivity },
-    { apply eq_pathover_constant_right, refine !functor_gluer ⬝ph _,
+    { apply eq_pathover, note x := functor_gluer2 f (λx : B, Point D) b, esimp [pconst] at *,
-      apply whisker_lb, apply square_of_eq, exact !ap_mk_left⁻¹ }
+      refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq,
+      rexact con.right_inv (gluel (f pt)) ⬝ (con.right_inv (gluer pt))⁻¹ }
   end
 
-  definition smash_functor_pconst_right [constructor] (f : A →* C) :
+  definition smash_functor_pconst_right (f : A →* C) :
     smash_functor f (pconst B D) ~* pconst (A ∧ B) (C ∧ D) :=
   begin
+    induction C with C, induction f with f f₀, esimp at *, induction f₀,
     fapply phomotopy.mk,
     { exact smash_functor_pconst_right_homotopy f },
-    { refine (ap_mk_left (respect_pt f))⁻¹ ⬝ _,
+    { rexact con.right_inv (gluel (f pt)) }
-      induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity }
+  end
+
+  -- example {X : Type*} {A B : Type} {a : A} (f : A → B) :
+  --   pmap_of_map f a ∘* pconst X _ = pconst X _ :=
+  -- idp
+
+  -- example {X : Type*} {A B : Type} {a : A} (f : A → B) :
+  --   @pcompose_pconst X _ _ (pmap_of_map f a) = sorry :=
+  -- begin unfold [pcompose_pconst] end
+
+
+  /- we need a coherence rule for smash_functor_pconst_right for the naturality of the
+    smash-pmap adjunction -/
+  private definition my_squarel {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₂ = a₃) :
+    square (p₁ ⬝ p₂⁻¹) p₂⁻¹ p₁ idp :=
+  proof square_of_eq idp qed
+
+  private definition my_squarer {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₁ = a₂) :
+    square (p₁ ⬝ p₁⁻¹) p₂⁻¹ p₂ idp :=
+  proof square_of_eq (con.right_inv p₁ ⬝ (con.right_inv p₂)⁻¹) qed
+
+  private definition my_cube_fillerl {A B C : Type} {g : B → C} {f : A → B} {a₁ a₂ : A} {b₀ : B}
+    {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) :
+    cube (hrfl ⬝hp (r a₁)⁻¹) hrfl
+         (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂)))
+         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹)
+           (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
+  begin
+    induction r using homotopy.rec_on_idp,
+    induction p using homotopy.rec_on_idp_left,
+    exact idc
+  end
+
+  private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B}
+    {pl : b₀ = bl} {pr : b₀ = br} {ql : g b₀ = g bl} {qr : g b₀ = g br}
+    (sl : ap g pl = ql) (sr : ap g pr = qr) :
+    cube (hrfl ⬝hp sr⁻¹) hrfl
+         (my_squarer ql qr) (aps g (my_squarer pl pr))
+         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ sl ◾ sl⁻²)⁻¹)
+         (hrfl ⬝hp sr⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
+  begin
+    induction sr,
+    induction sl,
+    induction pr,
+    induction pl,
+    exact idc
+  end
+
+  definition smash_functor_pconst_right_pcompose_homotopy {A B C D E F : Type}
+    (a₀ : A) (b₀ : B) (d₀ : D) (f' : C → E) (f : A → C) (g : D → F)
+    (x : pointed.MK A a₀ ∧ pointed.MK B b₀) :
+    square (smash_functor_pcompose_homotopy f' f g (λ a, d₀) x)
+    idp
+    (smash_functor_pconst_right_homotopy (λ a, f' (f a)) x)
+    (ap (smash_functor' (pmap.mk f' (refl (f' (f a₀)))) (pmap.mk g (refl (g d₀))))
+       (smash_functor_pconst_right_homotopy f x)) :=
+  begin
+    induction x with a b a b,
+    { refine _ ⬝hp (functor_gluel'2 f' g (f a) (f a₀))⁻¹, exact hrfl },
+    { refine _ ⬝hp !ap_inv⁻¹, refine _ ⬝hp !functor_gluel2⁻²⁻¹, exact hrfl },
+    { refine _ ⬝hp !ap_inv⁻¹, refine _ ⬝hp !functor_gluer2⁻²⁻¹, exact hrfl },
+    { exact abstract begin apply square_pathover,
+      refine !rec_eq_gluel ⬝p1 _ ⬝1p !natural_square_refl⁻¹,
+      refine !rec_eq_gluel ⬝p2 _ ⬝2p !natural_square_ap_fn⁻¹,
+      apply whisker001, apply whisker021,
+      apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹,
+      apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹,
+      refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (ap (aps _) !rec_eq_gluel ⬝ !aps_eq_hconcat)⁻¹,
+      apply whisker021, refine _ ⬝2p !aps_hconcat_eq⁻¹, apply move221,
+      refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹,
+      refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_ap_constant)),
+      apply my_cube_fillerl end end },
+    { exact abstract begin apply square_pathover,
+      refine !rec_eq_gluer ⬝p1 _ ⬝1p !natural_square_refl⁻¹,
+      refine !rec_eq_gluer ⬝p2 _ ⬝2p !natural_square_ap_fn⁻¹,
+      apply whisker001, apply whisker021,
+      apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹,
+      apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹,
+      refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (ap (aps _) !rec_eq_gluer ⬝ !aps_eq_hconcat)⁻¹,
+      apply whisker021, refine _ ⬝2p !aps_hconcat_eq⁻¹, apply move221,
+      refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹,
+      refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_ap_constant)), esimp,
+      apply my_cube_fillerr end end }
   end
 
   definition smash_functor_pconst_right_pcompose (f' : C →* E) (f : A →* C) (g : D →* F) :
@@ -211,7 +427,21 @@ namespace smash
              (pwhisker_left (smash_functor f' g) (smash_functor_pconst_right f) ⬝*
                pcompose_pconst (smash_functor f' g)) :=
   begin
-    exact sorry
+    induction A with A a₀, induction B with B b₀,
+    induction E with E e₀, induction C with C c₀, induction F with F x₀, induction D with D d₀,
+    induction f' with f' f'₀, induction f with f f₀, induction g with g g₀,
+    esimp at *, induction f'₀, induction f₀, induction g₀,
+    refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹,
+    fapply phomotopy_eq,
+    { intro x, refine eq_of_square _ ⬝ !con_idp,
+      exact smash_functor_pconst_right_pcompose_homotopy a₀ b₀ d₀ f' f g x, },
+    { refine _ ⬝ !idp_con⁻¹,
+      refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl_hconcat_eq) ⬝ _,
+      refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con, esimp,
+      refine whisker_right _ !functor_gluel'2_same ⬝ _,
+      refine !inv_con_cancel_right ⬝ _,
+      refine _ ⬝ idp ◾ ap (whisker_left _) (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹,
+      symmetry, apply whisker_left_idp }
   end
 
   definition smash_functor_pconst_right_pid_pcompose (g : D →* F) :

homotopy/smash_adjoint.hlean

@@ -48,12 +48,6 @@ namespace smash
     { apply eq_of_phomotopy, exact smash_pmap_unit_pt A B }
   end
 
-  definition smash_functor_pid_gluer' (A : Type*) {B C : Type*} (b : B) (f : B →* C) :
-    ap (smash_functor (pid A) f) (gluer' b pt) = gluer' (f b) (f pt) :=
-  begin
-    rexact functor_gluer'2 (@id A) f b pt
-  end
-
   definition smash_functor_pid_pinl' [constructor] {A B C : Type*} (b : B) (f : B →* C) :
     pinl A (f b) ~* smash_functor (pid A) f ∘* pinl A b :=
   begin
@@ -61,7 +55,7 @@ namespace smash
     { intro a, reflexivity },
     { refine !idp_con ⬝ _,
       induction C with C c₀, induction f with f f₀, esimp at *,
-      induction f₀, rexact smash_functor_pid_gluer' A b (pmap_of_map f pt) }
+      induction f₀, rexact functor_gluer'2 (@id A) f b pt }
   end
 
   definition smash_pmap_unit_pt_natural [constructor] (f : B →* C) :
@@ -79,7 +73,6 @@ namespace smash
     { refine whisker_right_idp _ ⬝ph _,
       refine ap (λx, _ ⬝ x) _ ⬝ph _,
       rotate 1, rexact (functor_gluel'2_same (pid A) f pt),
-      -- refine whisker_left _ (!con.assoc ⬝ whisker_left _ !con.left_inv ⬝ !con_idp) ⬝ph _,
       refine whisker_right _ !idp_con ⬝pv _,
       refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl,
       refine !con.assoc⁻¹ ⬝ whisker_right _ _ ⬝pv _,
@@ -91,7 +84,6 @@ namespace smash
       apply whisker_tl,
       apply vdeg_square,
       refine whisker_right _ !ap_inv ⬝ _, apply inv_con_eq_of_eq_con,
-      unfold [smash_functor_pid_gluer'],
       rexact functor_gluer'2_same (pmap_of_map id (Point A)) (pmap_of_map f pt) pt }
   end
 
@@ -482,4 +474,5 @@ namespace smash
   end
 
   print axioms smash_assoc
+
 end smash

move_to_lib.hlean

@@ -26,6 +26,145 @@ end algebra
 
 namespace eq
 
+section -- squares
+  variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A}
+            /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
+       {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
+            /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
+       {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
+            /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
+
+  variables {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁}
+            {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃}
+
+  definition natural_square_eq {A B : Type} {a a' : A} {f g : A → B} (p : f ~ g) (q : a = a')
+    : natural_square p q = square_of_pathover (apd p q) :=
+  idp
+
+  definition eq_of_square_hrfl_hconcat_eq {A : Type} {a a' : A} {p p' : a = a'} (q : p = p')
+    : eq_of_square (hrfl ⬝hp q⁻¹) = !idp_con ⬝ q :=
+  by induction q; induction p; reflexivity
+
+  definition aps_vrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') :
+    aps f (vrefl p) = vrefl (ap f p) :=
+  by induction p; reflexivity
+
+  definition aps_hrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') :
+    aps f (hrefl p) = hrefl (ap f p) :=
+  by induction p; reflexivity
+
+  definition natural_square_ap_fn {A B C : Type} {a a' : A} {g h : A → B} (f : B → C) (p : g ~ h) (q : a = a') :
+    natural_square (λa, ap f (p a)) q =
+      ap_compose f g q ⬝ph (aps f (natural_square p q) ⬝hp (ap_compose f h q)⁻¹) :=
+  begin
+    induction q, exact !aps_vrfl⁻¹
+  end
+
+  definition natural_square_refl {A B : Type} {a a' : A} (f : A → B) (q : a = a')
+    : natural_square (homotopy.refl f) q = hrfl :=
+  by induction q; reflexivity
+
+  definition aps_eq_hconcat {p₀₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) :
+    aps f (q ⬝ph s₁₁) = ap02 f q ⬝ph aps f s₁₁ :=
+  by induction q; reflexivity
+
+  definition aps_hconcat_eq {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁' = p₂₁) :
+    aps f (s₁₁ ⬝hp r⁻¹) = aps f s₁₁ ⬝hp (ap02 f r)⁻¹ :=
+  by induction r; reflexivity
+
+  definition aps_hconcat_eq' {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p₂₁') :
+    aps f (s₁₁ ⬝hp r) = aps f s₁₁ ⬝hp ap02 f r :=
+  by induction r; reflexivity
+
+  definition aps_square_of_eq (f : A → B) (s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) :
+    aps f (square_of_eq s) = square_of_eq ((ap_con f p₁₀ p₂₁)⁻¹ ⬝ ap02 f s ⬝ ap_con f p₀₁ p₁₂) :=
+  by induction p₁₂; esimp at *; induction s; induction p₂₁; induction p₁₀; reflexivity
+
+  definition aps_eq_hconcat_eq {p₀₁' p₂₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
+    (r : p₂₁' = p₂₁) : aps f (q ⬝ph s₁₁ ⬝hp r⁻¹) = ap02 f q ⬝ph aps f s₁₁ ⬝hp (ap02 f r)⁻¹ :=
+  by induction q; induction r; reflexivity
+
+end
+
+infix ` ⬝p2 `:75 := eq_concat2
+section -- cubes
+
+  variables {A B : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ a a' : A}
+            {p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂}
+            {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂}
+            {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂}
+            {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂}
+            {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁}
+            {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁}
+            {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
+            {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
+            {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
+            {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
+            {b₁ b₂ b₃ b₄ : B}
+            (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂)
+
+  definition whisker001 {p₀₀₁' : a₀₀₀ = a₀₀₂} (q : p₀₀₁' = p₀₀₁)
+    (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube (q ⬝ph s₀₁₁) s₂₁₁ (q ⬝ph s₁₀₁) s₁₂₁ s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+  definition whisker021 {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁' = p₀₂₁)
+    (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
+    cube (s₀₁₁ ⬝hp q⁻¹) s₂₁₁ s₁₀₁ (q ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+  definition whisker021' {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁ = p₀₂₁')
+    (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
+    cube (s₀₁₁ ⬝hp q) s₂₁₁ s₁₀₁ (q⁻¹ ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+  definition whisker201 {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁' = p₂₀₁)
+    (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
+    cube s₀₁₁ (q ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q⁻¹) s₁₂₁ s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+  definition whisker201' {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁ = p₂₀₁')
+    (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
+    cube s₀₁₁ (q⁻¹ ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+  definition whisker221 {p₂₂₁' : a₂₂₀ = a₂₂₂} (q : p₂₂₁ = p₂₂₁')
+    (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ (s₁₂₁ ⬝hp q) s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+  definition move221 {p₂₂₁' : a₂₂₀ = a₂₂₂} {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁'} (q : p₂₂₁ = p₂₂₁')
+    (c : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
+    cube s₀₁₁ s₂₁₁ s₁₀₁ (s₁₂₁ ⬝hp q⁻¹) s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+  definition move201 {p₂₀₁' : a₂₀₀ = a₂₀₂} {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁'}  (q : p₂₀₁' = p₂₀₁)
+    (c : cube s₀₁₁ (q ⬝ph s₂₁₁) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
+    cube s₀₁₁ s₂₁₁ (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ :=
+  by induction q; exact c
+
+end
+
+
+  definition apo011 {A : Type} {B C D : A → Type} {a a' : A} {p : a = a'} {b : B a} {b' : B a'}
+    {c : C a} {c' : C a'} (f : Π⦃a⦄, B a → C a → D a) (q : b =[p] b') (r : c =[p] c') :
+    f b c =[p] f b' c' :=
+  begin induction q, induction r using idp_rec_on, exact idpo end
+
+  definition ap011_ap_square_right {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a')
+    {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) :
+    square (ap011 f p q₁₂) (ap (λx, f x b₃) p) (ap (f a) q₁₃) (ap (f a') q₂₃) :=
+  by induction r; induction q₂₃; induction q₁₂; induction p; exact ids
+
+  definition ap011_ap_square_left {A B C : Type} (f : B → A → C) {a a' : A} (p : a = a')
+    {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) :
+    square (ap011 f q₁₂ p) (ap (f b₃) p) (ap (λx, f x a) q₁₃) (ap (λx, f x a') q₂₃) :=
+  by induction r; induction q₂₃; induction q₁₂; induction p; exact ids
+
+  definition ap_ap011 {A B C D : Type} (g : C → D) (f : A → B → C) {a a' : A} {b b' : B}
+    (p : a = a') (q : b = b') : ap g (ap011 f p q) = ap011 (λa b, g (f a b)) p q :=
+  begin
+    induction p, exact (ap_compose g (f a) q)⁻¹
+  end
+
   definition con2_assoc {A : Type} {x y z t : A} {p p' : x = y} {q q' : y = z} {r r' : z = t}
     (h : p = p') (h' : q = q') (h'' : r = r') :
     square ((h ◾ h') ◾ h'') (h ◾ (h' ◾ h'')) (con.assoc p q r) (con.assoc p' q' r') :=
@@ -144,6 +283,18 @@ namespace eq
   postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse
 
   end hsquare
+  -- move to init.funext
+  protected definition homotopy.rec_on_idp_left [recursor] {A : Type} {P : A → Type} {g : Πa, P a}
+    {Q : Πf, (f ~ g) → Type} {f : Π x, P x}
+    (p : f ~ g) (H : Q g (homotopy.refl g)) : Q f p :=
+  begin
+    induction p using homotopy.rec_on, induction q, exact H
+  end
+
+  --eq2
+  definition ap02_ap_constant {A B C : Type} {a a' : A} (f : B → C) (b : B) (p : a = a') :
+    square (ap_constant p (f b)) (ap02 f (ap_constant p b)) (ap_compose f (λx, b) p) idp :=
+  by induction p; exact ids
 
 end eq open eq
 
@@ -154,14 +305,44 @@ namespace wedge
 
 end wedge
 
+namespace pi
+
+  definition is_contr_pi_of_neg {A : Type} (B : A → Type) (H : ¬ A) : is_contr (Πa, B a) :=
+  begin
+    apply is_contr.mk (λa, empty.elim (H a)), intro f, apply eq_of_homotopy, intro x, contradiction
+  end
+end pi
+
 namespace pointed
 
+  -- FALSE
+  -- definition phomotopy_pconst {A B : Type*} {f : A →* B} (p q : f ~* pconst A B) : p = q :=
+  -- begin
+  --   induction f with f f₀,
+  --   induction p with p p₀, induction q with q q₀,
+  --   esimp at *, induction q₀,
+  -- end
+
+  definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A :=
+  begin
+    fapply phomotopy.mk,
+    { intro u, induction u, exact respect_pt f },
+    { reflexivity }
+  end
+
+  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)⁻¹*)
+
   definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : phomotopy_of_eq idp = phomotopy.refl f :=
   idp
 
   definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f :=
   λx, idp
 
+  definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) :
+    p a = q a :=
+  ap010 to_homotopy r a
+
   -- replace pcompose2 with this
   definition pcompose2' {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (q : g ~* g') (p : f ~* f') :
     g ∘* f ~* g' ∘* f' :=