Work on pointed naturality of smash-C

Notes/smash.tex

@@ -573,7 +573,7 @@ We define the pointed equivalences:
 \begin{thm}\label{thm:smash-functor-right}
 Given pointed types $A$, $B$ and $C$, the functorial action of the smash product induces a map
 $$({-})\smsh C:(A\pmap B)\pmap(A\smsh C\pmap B\smsh C)$$
-which is natural in $A$, $B$ and dinatural in $C$.
+which is natural in $A$, pointed natural in $B$ and dinatural in $C$.
 \end{thm}
 The naturality and dinaturality means that the following squares commute for $f : A' \to A$ $g:B\to B'$ and $h:C\to C'$.
 \begin{center}
@@ -614,8 +614,8 @@ fill the following square (after reducing out the applications of function exten
 \end{tikzcd}
 \end{center}
 The naturality in $B$ is almost the same: for the underlying homotopy we need to show
-$(g \o k)\smsh C = g\smsh C \o k\smsh C$. For the pointedness we need to fill the following
+$i:(g \o k)\smsh C = g\smsh C \o k\smsh C$. For the pointedness we need to fill the following
-square, which follows from \autoref{lem:smash-coh}.
+square, which follows from the left pentagon in \autoref{lem:smash-coh}.
 \begin{center}
 \begin{tikzcd}
 (g \o 0)\smsh C \arrow[r, equals]\arrow[dd,equals] &
@@ -625,6 +625,14 @@ square, which follows from \autoref{lem:smash-coh}.
 0
 \end{tikzcd}
 \end{center}
+To show that this naturality is pointed, we need to show that if $g=0$ then this homotopy is the same as the concatenation of the following pointed homotopies:
+$$q:({-})\smsh C \circ (A \to 0)\sim ({-})\smsh C \circ 0 \sim 0 \sim 0 \circ ({-})\smsh C\sim 0\smsh B \circ ({-})\smsh C.$$
+To show that the underlying homotopies are the same, we need to show that $i(0,f,\idfunc[C],\idfunc[C])$ is equal to the following concatenation of pointed homotopies
+$$q(f):(0\circ f)\smsh C\sim 0\smsh C \sim 0 \sim 0 \circ f\smsh C\sim 0\smsh B \circ f\smsh C,$$
+which is the right pentagons in \autoref{lem:smash-coh}. 
+To show that these pointed homotopies respect the basepoint in the same way, we need to show that (TODO)
+``$R\mathrel\square(0\smsh C \circ t)\cdot q_0=L$ where $L$ and $R$ are the left and right pentagons applied to $0$ and $\square$ is whiskering.''
+
 The dinaturality in $C$ is a bit harder. For the underlying homotopy we need to show
 $B\smsh h\o k\smsh C=k\smsh C'\o A\smsh h$. This follows by applying interchange twice:
 $$B\smsh h\o k\smsh C\sim(\idfunc[B]\o k)\smsh(h\o\idfunc[C])\sim(k\o\idfunc[A])\smsh(\idfunc[C']\o h)\sim k\smsh C'\o A\smsh h.$$
@@ -692,10 +700,9 @@ Note: $\eta$ is also dinatural in $B$, but we don't need this.
   $\epsilon (x):C$ by induction on $x$. If $x\jdeq(f,b)$ we set $\epsilon(f,b)\defeq f(b)$. If $x$
   is either $\auxl$ or $\auxr$ then we set $\epsilon (x)\defeq c_0:C$. If $x$ varies over $\gluel_f$
   then we need to show that $f(b_0)=c_0$, which is true by $f_0$. If $x$ varies over $\gluer_b$ we
-  need to show that $0(b)=c_0$ which is true by reflexivity. The map $\epsilon$ defined as such is trivially a pointed map,
+  need to show that $0(b)=c_0$ which is true by reflexivity. Now $\epsilon_0\defeq 1:\epsilon(0_{B,C},b_0)=c_0$ shows that $\epsilon$ is pointed.
-  which defines the counit.
 
-  Now we need to show that the unit and counit are (di)natural. (TODO).
+  Now we need to show that the counit is natural in $B$ and pointed natural in $C$.
 
   Finally, we need to show the unit-counit laws. For the underlying homotopy of the first one, let
   $f:A\to B$. We need to show that $p_f:\epsilon\o\eta f\sim f$. We define $p_f(a)=1:\epsilon(f,a)=f(a)$. To show that $p_f$ is a pointed homotopy, we need to show that
@@ -745,7 +752,7 @@ $$(A\pmap B\pmap C)\lpmap{({-})\smsh B}(A\smsh B\pmap (B\pmap C)\smsh B)\lpmap{A
 %   \end{align*}
 \end{proof}
 \begin{lem}\label{lem:e-natural}
-	The function $e$ is natural in $A$, $B$ and $C$.
+	The function $e$ is natural in $A$, $B$ and pointed natural in $C$.
 \end{lem}
 \begin{proof}
 	\textbf{Naturality of $e$ in $A$}. Suppose that $f:A'\pmap A$. Then the following diagram commutes. The left square commutes by naturality of $({-})\smsh B$ in the first argument and the right square commutes because composition on the left commutes with composition on the right.
@@ -771,6 +778,7 @@ $$(A\pmap B\pmap C)\lpmap{({-})\smsh B}(A\smsh B\pmap (B\pmap C)\smsh B)\lpmap{A
 		(A\smsh B\pmap C')
 	\end{tikzcd}
 	\end{center}
+Pointed naturality: TODO.
 
 	\textbf{Naturality of $e$ in $B$}. Suppose that $f:B'\pmap B$. Here the diagram is a bit more
 complicated, since $({-})\smsh B$ is dinatural (instead of natural) in $B$. Then we get the
@@ -796,15 +804,7 @@ argument, the back square commutes because composition on the left commutes with
   inductive type to prove that.
 \end{rmk}
 
-\begin{lem}\label{lem:e-pointed-natural}
+\section{Symmetric monoid product}
-	The function $e$ is pointed natural in $C$.
-\end{lem}
-
-\begin{proof}
-	(TODO)
-\end{proof}
-
-\section{Symmetric monoidality}
 We aim to prove that the smash product is a (1-coherent) symmetric monoidal product [REF: Brunerie] for pointed types, i.e., that
 \[(\type^*,\, \bool,\, \smsh,\, \alpha,\, \lambda,\, \rho,\, \gamma)\]
 is a symmetric monoidal category, with the type of booleans $\bool$ (pointed in $0_\bool$) as unit, and for suitable instances of $\alpha$, $\lambda$, $\rho$ and $\gamma$ witnessing associativity, left- and right unitality and the braiding for $\smsh$ and satisfying appropriate coherence relations (associativity pentagon; unitors triangle; braiding-unitors triangle; associativity-braiding hexagon; double braiding).

algebra/quotient_group.hlean

@@ -723,7 +723,7 @@ namespace group
     (hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) :
     quotient_ab_group_functor ψ hψ ∘g quotient_ab_group_functor φ hφ ~
     quotient_ab_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
-  @quotient_group_functor_compose G H K R _ S _ T _ ψ φ  hψ hφ 
+  @quotient_group_functor_compose G H K R _ S _ T _ ψ φ  hψ hφ
 
   definition quotient_ab_group_functor_gid :
     quotient_ab_group_functor (gid G) (λg, id) ~ gid (quotient_ab_group R) :=

homotopy/EM.hlean

@@ -655,8 +655,21 @@ namespace EM
   definition cokernel {G H : AbGroup} (φ : G →g H) : AbGroup :=
   quotient_ab_group (image φ)
 
+  /- todo: in algebra/quotient_group, do the first steps without assuming that N is normal,
+  then this is qg for (image φ) in H -/
+  definition image_cosets {G H : Group} (φ : G →g H) : Set* :=
+  sorry
+
+  definition homotopy_group_EMadd1_functor1 {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+    πg[n+1] (pfiber (EMadd1_functor φ (n+1))) ≃g cokernel φ :=
+  sorry
+
+  definition homotopy_group_EMadd1_functor2 {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+    πg[n+1] (pfiber (EMadd1_functor φ n)) ≃g Kernel φ :=
+  sorry
+
   definition trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) :
-    ptrunc 0 (pfiber (EM1_functor φ)) ≃* sorry :=
+    ptrunc 0 (pfiber (EM1_functor φ)) ≃* image_cosets φ :=
   sorry
 
 end EM

homotopy/smash.hlean

@@ -1,6 +1,6 @@
 -- Authors: Floris van Doorn
 
-import homotopy.smash types.pointed2 .pushout homotopy.red_susp
+import homotopy.smash types.pointed2 .pushout homotopy.red_susp ..pointed
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
      function red_susp unit
@@ -536,14 +536,15 @@ namespace smash
     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}
+  private definition my_cube_fillerl {B C : Type} {g : B → C} {fa₁ fa₂ b₀ : B}
-    {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) :
+    {pa₁ : fa₁ = b₀} {pa₂ : fa₂ = b₀} {qa₁ : g (fa₁) = g b₀} {qa₂ : g (fa₂) = g b₀}
-    cube (hrfl ⬝hp (r a₁)⁻¹) hrfl
+    (ra₁ : ap g (pa₁) = qa₁) (ra₂ : ap g (pa₂) = qa₂) :
-         (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂)))
+    cube (hrfl ⬝hp (ra₁)⁻¹) hrfl
-         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹)
+         (my_squarel (qa₁) (qa₂)) (aps g (my_squarel (pa₁) (pa₂)))
-           (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
+         (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (ra₁) ◾ (ra₂)⁻²)⁻¹)
+           (hrfl ⬝hp (ra₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) :=
   begin
-    induction r using homotopy.rec_on_idp, induction p using homotopy.rec_on_idp_left, exact idc
+    induction ra₂, induction ra₁, induction pa₂, induction pa₁, exact idc
   end
 
   private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B}
@@ -615,11 +616,11 @@ namespace smash
       refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con,
       refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluer'2_same f' g' (g b₀),
       refine !inv_con_cancel_right ⬝ _,
-      exact sorry, -- TODO: FIX, the proof below should work (with some small changes)
+      refine !whisker_left_idp⁻¹ ⬝ _,
-      -- refine _ ⬝ whisker_left _ _,
+      refine !con_idp ⬝ _,
-      -- rotate 2, refine ap (whisker_left _) _, symmetry, exact !idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con,
+      apply whisker_left,
-      -- symmetry, apply whisker_left_idp
+      apply ap (whisker_left idp),
-      }
+      exact (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹ }
   end
 
   /- a version where the left maps are identities -/
@@ -725,7 +726,7 @@ namespace smash
 
   /- Using these lemmas we show that smash_functor_left is natural in all arguments -/
 
-  definition smash_functor_left_natural_left (f : A' →* A) :
+  definition smash_functor_left_natural_left (B C : Type*) (f : A' →* A) :
     psquare (smash_functor_left A B C) (smash_functor_left A' B C)
             (ppcompose_right f) (ppcompose_right (f ∧→ pid C)) :=
   begin
@@ -739,7 +740,7 @@ namespace smash
       apply smash_functor_pcompose_pconst1_pid }
   end
 
-  definition smash_functor_left_natural_middle (f : B →* B') :
+  definition smash_functor_left_natural_middle (A C : Type*) (f : B →* B') :
     psquare (smash_functor_left A B C) (smash_functor_left A B' C)
             (ppcompose_left f) (ppcompose_left (f ∧→ pid C)) :=
   begin
@@ -753,7 +754,7 @@ namespace smash
       apply smash_functor_pcompose_pconst2_pid }
   end
 
-  definition smash_functor_left_natural_right (f : C →* C') :
+  definition smash_functor_left_natural_right (A B : Type*) (f : C →* C') :
     psquare (smash_functor_left A B C) (ppcompose_right (pid A ∧→ f))
             (smash_functor_left A B C') (ppcompose_left (pid B ∧→ f)) :=
   begin
@@ -772,6 +773,18 @@ namespace smash
       refine idp ◾** !refl_trans ⬝ !trans_left_inv }
   end
 
+  definition smash_functor_left_natural_middle_phomotopy (A C : Type*) {f f' : B →* B'}
+    (p : f ~* f') : smash_functor_left_natural_middle A C f =
+    ppcompose_left_phomotopy p ⬝ph* smash_functor_left_natural_middle A C f' ⬝hp*
+    ppcompose_left_phomotopy (p ∧~ phomotopy.rfl) :=
+  begin
+    induction p using phomotopy_rec_idp,
+    symmetry,
+    refine !ppcompose_left_phomotopy_refl ◾ph* idp ◾hp*
+     (ap ppcompose_left_phomotopy !smash_functor_phomotopy_refl ⬝
+     !ppcompose_left_phomotopy_refl) ⬝ _,
+    exact !rfl_phomotopy_hconcat ⬝ !hconcat_phomotopy_rfl
+  end
 
   /- the following is not really used, but a symmetric version of the natural equivalence
      smash_functor_left -/
@@ -877,11 +890,11 @@ namespace smash
       refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con,
       refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluel'2_same f' g (f a₀),
       refine !inv_con_cancel_right ⬝ _,
-      exact sorry, -- TODO: FIX, the proof below should work
+      refine !whisker_left_idp⁻¹ ⬝ _,
-      -- refine _ ⬝ whisker_left _ _,
+      refine !con_idp ⬝ _,
-      -- rotate 2, refine ap (whisker_left _) _, symmetry, exact !idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con,
+      apply whisker_left,
-      -- symmetry, apply whisker_left_idp
+      apply ap (whisker_left idp),
-      }
+      exact (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹ }
   end
 
   /- a version where the left maps are identities -/
@@ -985,7 +998,7 @@ namespace smash
   smash_functor_pcompose_pconst3 (pid A) (pid A) g
 
   /- Using these lemmas we show that smash_functor_right is natural in all arguments -/
-  definition smash_functor_right_natural_right (f : C →* C') :
+  definition smash_functor_right_natural_right (A B : Type*) (f : C →* C') :
     psquare (smash_functor_right A B C) (smash_functor_right A B C')
             (ppcompose_left f) (ppcompose_left (pid A ∧→ f)) :=
   begin
@@ -999,7 +1012,7 @@ namespace smash
       apply smash_functor_pcompose_pconst4_pid }
   end
 
-  definition smash_functor_right_natural_middle (f : B' →* B) :
+  definition smash_functor_right_natural_middle (A C : Type*) (f : B' →* B) :
     psquare (smash_functor_right A B C) (smash_functor_right A B' C)
             (ppcompose_right f) (ppcompose_right (pid A ∧→ f)) :=
   begin
@@ -1013,7 +1026,7 @@ namespace smash
       apply smash_functor_pcompose_pconst3_pid }
   end
 
-  definition smash_functor_right_natural_left (f : A →* A') :
+  definition smash_functor_right_natural_left (B C : Type*) (f : A →* A') :
     psquare (smash_functor_right A B C) (ppcompose_right (f ∧→ (pid B)))
             (smash_functor_right A' B C) (ppcompose_left (f ∧→ (pid C))) :=
   begin

homotopy/smash_adjoint.hlean

@@ -53,8 +53,10 @@ namespace smash
   end
 
   definition smash_pmap_unit_pt_natural [constructor] (B : Type*) (f : A →* A') :
-    smash_functor_pid_pinr' B f pt ⬝* pwhisker_left (smash_functor f (pid B)) (smash_pmap_unit_pt A B) ⬝*
+    smash_functor_pid_pinr' B f pt ⬝*
-      pcompose_pconst (f ∧→ (pid B)) = pinr_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A' B :=
+    pwhisker_left (smash_functor f (pid B)) (smash_pmap_unit_pt A B) ⬝*
+    pcompose_pconst (f ∧→ (pid B)) =
+    pinr_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A' B :=
   begin
     induction f with f f₀, induction A' with A' a₀', esimp at *,
     induction f₀, refine _ ⬝ !refl_trans⁻¹,
@@ -147,7 +149,7 @@ namespace smash
       refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ }
   end
 
-  definition smash_pmap_counit_natural_left (g : B →* B') :
+  definition smash_pmap_counit_natural_left (C : Type*) (g : B →* B') :
     psquare (pid (ppmap B' C) ∧→ g) (smash_pmap_counit B C)
             (ppcompose_right g ∧→ pid B) (smash_pmap_counit B' C) :=
   begin
@@ -336,20 +338,20 @@ namespace smash
   definition smash_pelim_natural_left (B C : Type*) (f : A' →* A) :
     psquare (smash_pelim A B C) (smash_pelim A' B C)
             (ppcompose_right f) (ppcompose_right (f ∧→ pid B)) :=
-  smash_functor_left_natural_left f ⬝h* !ppcompose_left_ppcompose_right
+  smash_functor_left_natural_left (ppmap B C) B f ⬝h* !ppcompose_left_ppcompose_right
 
   definition smash_pelim_natural_middle (A C : Type*) (f : B' →* B) :
     psquare (smash_pelim A B C) (smash_pelim A B' C)
             (ppcompose_left (ppcompose_right f)) (ppcompose_right (pid A ∧→ f)) :=
   pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝*
   (!smash_functor_left_natural_right⁻¹* ⬝pv*
-  smash_functor_left_natural_middle (ppcompose_right f) ⬝h*
+  smash_functor_left_natural_middle _ _ (ppcompose_right f) ⬝h*
   ppcompose_left_psquare !smash_pmap_counit_natural_left)
 
-  definition smash_pelim_natural_right (f : C →* C') :
+  definition smash_pelim_natural_right (A B : Type*) (f : C →* C') :
     psquare (smash_pelim A B C) (smash_pelim A B C')
             (ppcompose_left (ppcompose_left f)) (ppcompose_left f) :=
-  smash_functor_left_natural_middle (ppcompose_left f) ⬝h*
+  smash_functor_left_natural_middle _ _ (ppcompose_left f) ⬝h*
   ppcompose_left_psquare (smash_pmap_counit_natural_right _ f)
 
   definition smash_pelim_natural_lm (C : Type*) (f : A' →* A) (g : B' →* B) :
@@ -393,28 +395,29 @@ namespace smash
     (smash_adjoint_pmap A B C')⁻¹ᵉ* (ppcompose_left f ∘* g) :=
   smash_elim_natural_right f g
 
-   definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') :
+   definition smash_adjoint_pmap_inv_natural_right [constructor] (A B : Type*) (f : C →* C') :
-    ppcompose_left f ∘* smash_adjoint_pmap_inv A B C ~*
+    psquare (smash_adjoint_pmap_inv A B C) (smash_adjoint_pmap_inv A B C')
-    smash_adjoint_pmap_inv A B C' ∘* ppcompose_left (ppcompose_left f) :=
+            (ppcompose_left (ppcompose_left f)) (ppcompose_left f) :=
-  smash_pelim_natural_right f
+  smash_pelim_natural_right A B f
 
-  definition smash_adjoint_pmap_natural_right [constructor] {A B C C' : Type*} (f : C →* C') :
+  definition smash_adjoint_pmap_natural_right [constructor] (A B : Type*) (f : C →* C') :
-    ppcompose_left (ppcompose_left f) ∘* smash_adjoint_pmap A B C ~*
+    psquare (smash_adjoint_pmap A B C) (smash_adjoint_pmap A B C')
-    smash_adjoint_pmap A B C' ∘* ppcompose_left f :=
+            (ppcompose_left f) (ppcompose_left (ppcompose_left f)) :=
-  (smash_adjoint_pmap_inv_natural_right f)⁻¹ʰ*
+  (smash_adjoint_pmap_inv_natural_right A B f)⁻¹ʰ*
 
   definition smash_adjoint_pmap_natural_lm (C : Type*) (f : A →* A') (g : B →* B') :
     psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C)
             (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) :=
   (smash_pelim_natural_lm C f g)⁻¹ʰ*
 
+  /- some naturalities we skipped, but are now easier to prove -/
   definition smash_elim_inv_natural_middle (f : B' →* B)
     (g : A ∧ B →* C) : ppcompose_right f ∘* smash_elim_inv g ~* smash_elim_inv (g ∘* pid A ∧→ f) :=
   !pcompose_pid⁻¹* ⬝* !passoc ⬝* phomotopy_of_eq (smash_adjoint_pmap_natural_lm C (pid A) f g)
 
   definition smash_pmap_unit_natural_left (f : B →* B') :
-    ppcompose_left (pid A ∧→ f) ∘* smash_pmap_unit A B ~*
+    psquare (smash_pmap_unit A B) (ppcompose_right f)
-    ppcompose_right f ∘* smash_pmap_unit A B' :=
+            (smash_pmap_unit A B') (ppcompose_left (pid A ∧→ f)) :=
   begin
     refine pwhisker_left _ !smash_pelim_inv_pid⁻¹* ⬝* _ ⬝* pwhisker_left _ !smash_pelim_inv_pid,
     refine !smash_elim_inv_natural_right ⬝* _ ⬝* !smash_elim_inv_natural_middle⁻¹*,
@@ -461,7 +464,17 @@ namespace smash
 
   definition smash_assoc_elim_natural_right_pt (f : X →* X') (g : A ∧ (B ∧ C) →* X) :
     f ∘* smash_assoc_elim_pequiv A B C X g ~* smash_assoc_elim_pequiv A B C X' (f ∘* g) :=
-  phomotopy_of_eq (smash_assoc_elim_natural_right A B C f g)
+  begin
+    refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _,
+    apply smash_elim_phomotopy,
+    refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _,
+    apply smash_elim_phomotopy,
+    refine !passoc⁻¹* ⬝* _,
+    refine pwhisker_right _ !smash_adjoint_pmap_natural_right ⬝* _,
+    refine !passoc ⬝* _,
+    apply pwhisker_left,
+    refine !smash_adjoint_pmap_natural_right_pt
+  end
 
   definition smash_assoc_elim_inv_natural_right_pt (f : X →* X') (g : (A ∧ B) ∧ C →* X) :
     f ∘* (smash_assoc_elim_pequiv A B C X)⁻¹ᵉ* g ~*
@@ -517,9 +530,9 @@ namespace smash
   definition smash_assoc_elim_right_natural_right (A B C D : Type*) (f : X →* X') :
     psquare (smash_assoc_elim_right_pequiv A B C D X) (smash_assoc_elim_right_pequiv A B C D X')
             (ppcompose_left f) (ppcompose_left f) :=
-  smash_adjoint_pmap_natural_right f ⬝h*
+  smash_adjoint_pmap_natural_right (A ∧ (B ∧ C)) D f ⬝h*
   smash_assoc_elim_natural_right A B C (ppcompose_left f) ⬝h*
-  smash_adjoint_pmap_inv_natural_right f
+  smash_adjoint_pmap_inv_natural_right ((A ∧ B) ∧ C) D f
 
   definition smash_assoc_smash_functor (A B C D : Type*) :
     smash_assoc A B C ∧→ pid D ~* !smash_assoc_elim_right_pequiv (pid _) :=
@@ -534,7 +547,7 @@ namespace smash
 
   definition ppcompose_right_smash_assoc (A B C X : Type*) :
     ppcompose_right (smash_assoc A B C) ~* smash_assoc_elim_pequiv A B C X :=
-  sorry -- one hole left
+  sorry
 
   definition smash_functor_smash_assoc (A B C D : Type*) :
     pid A ∧→ smash_assoc B C D ~* !smash_assoc_elim_left_pequiv (pid _) :=
@@ -543,7 +556,7 @@ namespace smash
     refine pap (!smash_adjoint_pmap_inv ∘* ppcompose_left _) !smash_pelim_inv_pid ⬝* _,
     refine pap !smash_adjoint_pmap_inv (pwhisker_right _ !ppcompose_right_smash_assoc⁻¹* ⬝*
       !smash_pmap_unit_natural_left⁻¹*) ⬝* _,
-    refine phomotopy_of_eq (smash_adjoint_pmap_inv_natural_right (pid A ∧→ smash_assoc B C D)
+    refine phomotopy_of_eq (smash_adjoint_pmap_inv_natural_right _ _ (pid A ∧→ smash_assoc B C D)
       !smash_pmap_unit)⁻¹ ⬝* _,
     refine pwhisker_left _ _ ⬝* !pcompose_pid,
     apply smash_pmap_unit_counit
@@ -589,10 +602,10 @@ namespace smash
   definition smash_susp_elim_natural_right (A B : Type*) (f : X →* X') :
     psquare (smash_susp_elim_pequiv A B X) (smash_susp_elim_pequiv A B X')
             (ppcompose_left f) (ppcompose_left f) :=
-  smash_adjoint_pmap_natural_right f ⬝h*
+  smash_adjoint_pmap_natural_right (⅀ A) B f ⬝h*
   susp_adjoint_loop_natural_right (ppcompose_left f) ⬝h*
   ppcompose_left_psquare (loop_pmap_commute_natural_right B f) ⬝h*
-  (smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h*
+  (smash_adjoint_pmap_natural_right A B (Ω→ f))⁻¹ʰ* ⬝h*
   (susp_adjoint_loop_natural_right f)⁻¹ʰ*
 
   definition smash_susp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) :
@@ -640,6 +653,11 @@ namespace smash
         ... ≃* ⅀(B ∧ A) : susp_smash B A
         ... ≃* ⅀(A ∧ B) : susp_pequiv (smash_comm B A)
 
+
+  definition smash_susp_natural (f : A →* A') (g : B →* B') :
+    psquare (smash_susp A B) (smash_susp A' B') (f ∧→ ⅀→g) (⅀→ (f ∧→ g)) :=
+  sorry
+
   definition susp_smash_move (A B : Type*) : ⅀ A ∧ B ≃* A ∧ ⅀ B :=
   susp_smash A B ⬝e* (smash_susp A B)⁻¹ᵉ*
 

move_to_lib.hlean

@@ -932,6 +932,9 @@ namespace is_conn
   definition is_conn_zero_pointed {A : Type*} (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A :=
   is_conn_zero (tr pt) p
 
+  definition is_conn_zero_pointed' {A : Type*} (p : Πa : A, ∥ a = pt ∥) : is_conn 0 A :=
+  is_conn_zero_pointed (λa a', tconcat (p a) (tinverse (p a')))
+
   definition is_conn_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) [is_conn n A] [is_conn (n.+1) B] :
     is_conn n (fiber f b) :=
   is_conn_equiv_closed_rev _ !fiber.sigma_char _
@@ -951,10 +954,8 @@ namespace misc
   pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩
 
   lemma is_conn_component [instance] (A : Type*) : is_conn 0 (component A) :=
-  is_contr.mk (tr pt)
+  is_conn_zero_pointed'
-    begin
+    begin intro x, induction x with a p, induction p with p, induction p, exact tidp end
-      intro x, induction x with x, induction x with a p, induction p with p, induction p, reflexivity
-    end
 
   definition component_incl [constructor] (A : Type*) : component A →* A :=
   pmap.mk pr1 idp

pointed.hlean

@@ -8,6 +8,43 @@ open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma gr
 
 namespace pointed
 
+  definition phomotopy_mk_eq {A B : Type*} {f g : A →* B} {h k : f ~ g}
+    {h₀ : h pt ⬝ respect_pt g = respect_pt f} {k₀ : k pt ⬝ respect_pt g = respect_pt f} (p : h ~ k)
+    (q : whisker_right (respect_pt g) (p pt) ⬝ k₀ = h₀) : phomotopy.mk h h₀ = phomotopy.mk k k₀ :=
+  phomotopy_eq p (idp ◾ to_right_inv !eq_con_inv_equiv_con_eq _ ⬝
+    q ⬝ (to_right_inv !eq_con_inv_equiv_con_eq _)⁻¹)
+
+
+  section phsquare
+  /-
+    Squares of pointed homotopies
+  -/
+
+  variables {A : Type*} {P : A → Type} {p₀ : P pt}
+            {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₄₂}
+            {p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄}
+            {p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄}
+
+  definition phtranspose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₀₁ p₂₁ p₁₀ p₁₂ :=
+  p⁻¹
+
+  definition eq_top_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ = p₀₁ ⬝* p₁₂ ⬝* p₂₁⁻¹* :=
+  eq_trans_symm_of_trans_eq p
+
+  definition eq_bot_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₂ = p₀₁⁻¹* ⬝* p₁₀ ⬝* p₂₁ :=
+  eq_symm_trans_of_trans_eq p⁻¹ ⬝ !trans_assoc⁻¹
+
+  definition eq_left_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₀₁ = p₁₀ ⬝* p₂₁ ⬝* p₁₂⁻¹* :=
+  eq_top_of_phsquare (phtranspose p)
+
+  definition eq_right_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₂₁ = p₁₀⁻¹* ⬝* p₀₁ ⬝* p₁₂ :=
+  eq_bot_of_phsquare (phtranspose p)
+
+  end phsquare
+
   -- /- the pointed type of (unpointed) dependent maps -/
   -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
   -- pointed.mk' (Πa, P a)
@@ -33,12 +70,32 @@ namespace pointed
   --     apply equiv_eq_closed_right, exact !idp_con⁻¹ }
   -- end
 
+
+  /- todo: make type argument explicit in ppcompose_left and ppcompose_left_* -/
+  /- todo: delete papply_pcompose -/
+  /- todo: pmap_pbool_equiv is a special case of ppmap_pbool_pequiv. -/
+
   definition ppcompose_left_pid [constructor] (A B : Type*) : ppcompose_left (pid B) ~* pid (ppmap A B) :=
   phomotopy_mk_ppmap (λf, pid_pcompose f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹)
 
   definition ppcompose_right_pid [constructor] (A B : Type*) : ppcompose_right (pid A) ~* pid (ppmap A B) :=
   phomotopy_mk_ppmap (λf, pcompose_pid f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹)
 
+  section
+  variables {A A' : Type*} {P : A → Type} {P' : A' → Type} {p₀ : P pt} {p₀' : P' pt} {k l : ppi P p₀}
+  definition phomotopy_of_eq_inv (p : k = l) :
+    phomotopy_of_eq p⁻¹ = (phomotopy_of_eq p)⁻¹* :=
+  begin induction p, exact !refl_symm⁻¹ end
+
+  /- todo: replace regular pap -/
+  definition pap' (f : ppi P p₀ → ppi P' p₀') (p : k ~* l) : f k ~* f l :=
+  by induction p using phomotopy_rec_idp; reflexivity
+
+  definition phomotopy_of_eq_ap (f : ppi P p₀ → ppi P' p₀') (p : k = l) :
+    phomotopy_of_eq (ap f p) = pap' f (phomotopy_of_eq p) :=
+  begin induction p, exact !phomotopy_rec_idp_refl⁻¹ end
+  end
+
   /- remove some duplicates: loop_ppmap_commute, loop_ppmap_pequiv, loop_ppmap_pequiv', pfunext -/
   definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
   (loop_ppmap_commute X Y)⁻¹ᵉ*
@@ -147,13 +204,69 @@ namespace pointed
 
 /- Homotopy between a function and its eta expansion -/
 
-  definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) :=
+  definition pmap_eta [constructor] {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) :=
   begin
     fapply phomotopy.mk,
     reflexivity,
     esimp, exact !idp_con
   end
 
+  definition papply_point [constructor] (A B : Type*) : papply B pt ~* pconst (ppmap A B) B :=
+  phomotopy.mk (λf, respect_pt f) idp
+
+  definition pmap_swap_map [constructor] {A B C : Type*} (f : A →* ppmap B C) :
+    ppmap B (ppmap A C) :=
+  begin
+    fapply pmap.mk,
+    { intro b, exact papply C b ∘* f },
+    { apply eq_of_phomotopy, exact pwhisker_right f (papply_point B C) ⬝* !pconst_pcompose }
+  end
+
+  definition pmap_swap_map_pconst (A B C : Type*) :
+    pmap_swap_map (pconst A (ppmap B C)) ~* pconst B (ppmap A C) :=
+  begin
+    fapply phomotopy_mk_ppmap,
+    { intro b, reflexivity },
+    { refine !refl_trans ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ }
+  end
+
+  definition papply_pmap_swap_map [constructor] {A B C : Type*} (f : A →* ppmap B C) (a : A) :
+    papply C a ∘* pmap_swap_map f ~* f a :=
+  begin
+    fapply phomotopy.mk,
+    { intro b, reflexivity },
+    { exact !idp_con ⬝ !ap_eq_of_phomotopy⁻¹ }
+  end
+
+  definition pmap_swap_map_pmap_swap_map {A B C : Type*} (f : A →* ppmap B C) :
+    pmap_swap_map (pmap_swap_map f) ~* f :=
+  begin
+    fapply phomotopy_mk_ppmap,
+    { exact papply_pmap_swap_map f },
+    { refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
+      fapply phomotopy_mk_eq, intro b, exact !idp_con,
+      refine !whisker_right_idp ◾ (!idp_con ◾ idp) ⬝ _ ⬝ !idp_con⁻¹ ◾ idp,
+      symmetry, exact sorry }
+  end
+
+  definition pmap_swap [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap B (ppmap A C) :=
+  begin
+    fapply pmap.mk,
+    { exact pmap_swap_map },
+    { exact eq_of_phomotopy (pmap_swap_map_pconst A B C) }
+  end
+
+  definition pmap_swap_pequiv [constructor] (A B C : Type*) :
+    ppmap A (ppmap B C) ≃* ppmap B (ppmap A C) :=
+  begin
+    fapply pequiv_of_pmap,
+    { exact pmap_swap A B C },
+    fapply adjointify,
+    { exact pmap_swap B A C },
+    { intro f, apply eq_of_phomotopy, exact pmap_swap_map_pmap_swap_map f },
+    { intro f, apply eq_of_phomotopy, exact pmap_swap_map_pmap_swap_map f }
+  end
+
   -- this should replace pnatural_square
   definition pnatural_square2 {A B : Type} (X : B → Type*) (Y : B → Type*) {f g : A → B}
     (h : Πa, X (f a) →* Y (g a)) {a a' : A} (p : a = a') :
@@ -176,10 +289,39 @@ namespace pointed
   section psquare
   variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
             {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
-            {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
+            {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ f₄₁' : A₄₀ →* A₄₂}
             {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
             {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
-            {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
+            {f₁₄ f₁₄' : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
+
+  definition phconst_square (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) :
+    psquare (pconst A₀₀ A₂₀) (pconst A₀₂ A₂₂) f₀₁ f₂₁ :=
+  !pcompose_pconst ⬝* !pconst_pcompose⁻¹*
+
+  definition pvconst_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) :
+    psquare f₁₀ f₁₂ (pconst A₀₀ A₀₂) (pconst A₂₀ A₂₂) :=
+  !pconst_pcompose ⬝* !pcompose_pconst⁻¹*
+
+  definition pvconst_square_pcompose (f₃₀ : A₂₀ →* A₄₀) (f₁₀ : A₀₀ →* A₂₀)
+    (f₃₂ : A₂₂ →* A₄₂) (f₁₂ : A₀₂ →* A₂₂) :
+    pvconst_square (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) = pvconst_square f₁₀ f₁₂ ⬝h* pvconst_square f₃₀ f₃₂ :=
+  begin
+    refine eq_right_of_phsquare !passoc_pconst_left ◾** !passoc_pconst_right⁻¹⁻²** ⬝ idp ◾**
+      (!trans_symm ⬝ !trans_symm ◾** idp) ⬝ !trans_assoc⁻¹ ⬝ _ ◾** idp,
+    refine !trans_assoc⁻¹ ⬝ _ ◾** !pwhisker_left_symm⁻¹ ⬝ !trans_assoc ⬝
+      idp ◾** !pwhisker_left_trans⁻¹,
+    apply trans_symm_eq_of_eq_trans,
+    refine _ ⬝ idp ◾** !passoc_pconst_middle⁻¹ ⬝ !trans_assoc⁻¹ ⬝ !trans_assoc⁻¹,
+    refine _ ◾** idp ⬝ !trans_assoc,
+    refine idp ◾** _ ⬝ !trans_assoc⁻¹,
+    refine ap (pwhisker_right f₁₀) _ ⬝ !pwhisker_right_trans,
+    refine !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹,
+  end
+
+  definition phconst_square_pcompose (f₀₃ : A₀₂ →* A₀₄) (f₁₀ : A₀₀ →* A₂₀)
+    (f₂₃ : A₂₂ →* A₂₄) (f₂₁ : A₂₀ →* A₂₂) :
+    phconst_square (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₁₂) = phconst_square f₀₁ f₁₂ ⬝v* phconst_square f₀₃ f₂₃ :=
+  sorry
 
   definition ptranspose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ :=
   p⁻¹*
@@ -187,9 +329,94 @@ namespace pointed
   definition hsquare_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ :=
   p
 
-  definition homotopy_group_functor_hsquare (n : ℕ) (h : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+  definition rfl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p :=
-    psquare (π→[n] f₁₀) (π→[n] f₁₂)
+  idp ◾** (ap (pwhisker_left f₁₂) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl
-            (π→[n] f₀₁) (π→[n] f₂₁) :=
+
+  definition hconcat_phomotopy_rfl (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : p ⬝hp* phomotopy.rfl = p :=
+  !pwhisker_right_refl ◾** idp ⬝ !refl_trans
+
+  definition rfl_phomotopy_vconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝pv* p = p :=
+  !pwhisker_left_refl ◾** idp ⬝ !refl_trans
+
+  definition vconcat_phomotopy_rfl (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : p ⬝vp* phomotopy.rfl = p :=
+  idp ◾** (ap (pwhisker_right f₀₁) !refl_symm ⬝ !pwhisker_right_refl) ⬝ !trans_refl
+
+  definition phomotopy_hconcat_phconcat (p : f₀₁' ~* f₀₁) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (r : psquare f₃₀ f₃₂ f₂₁ f₄₁) : (p ⬝ph* q) ⬝h* r = p ⬝ph* (q ⬝h* r) :=
+  begin
+    induction p using phomotopy_rec_idp,
+    exact !refl_phomotopy_hconcat ◾h* idp ⬝ !refl_phomotopy_hconcat⁻¹
+  end
+
+  definition phconcat_hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) (r : f₄₁' ~* f₄₁) : (p ⬝h* q) ⬝hp* r = p ⬝h* (q ⬝hp* r) :=
+  begin
+    induction r using phomotopy_rec_idp,
+    exact !hconcat_phomotopy_rfl ⬝ idp ◾h* !hconcat_phomotopy_rfl⁻¹
+  end
+
+  definition phomotopy_hconcat_phomotopy (p : f₀₁' ~* f₀₁) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (r : f₂₁' ~* f₂₁) : (p ⬝ph* q) ⬝hp* r = p ⬝ph* (q ⬝hp* r) :=
+  begin
+    induction r using phomotopy_rec_idp,
+    exact !hconcat_phomotopy_rfl ⬝ idp ◾ph* !hconcat_phomotopy_rfl⁻¹
+  end
+
+  definition hconcat_phomotopy_phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (q : f₂₁' ~* f₂₁) (r : psquare f₃₀ f₃₂ f₂₁' f₄₁) : (p ⬝hp* q) ⬝h* r = p ⬝h* (q⁻¹* ⬝ph* r) :=
+  begin
+    induction q using phomotopy_rec_idp,
+    exact !hconcat_phomotopy_rfl ◾h* idp ⬝ idp ◾h* (!refl_symm ◾ph* idp ⬝ !refl_phomotopy_hconcat)⁻¹
+  end
+
+  definition phconcat_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (q : f₂₁ ~* f₂₁') (r : psquare f₃₀ f₃₂ f₂₁' f₄₁) : p ⬝h* (q ⬝ph* r) = (p ⬝hp* q⁻¹*) ⬝h* r :=
+  begin
+    induction q using phomotopy_rec_idp,
+    exact idp ◾h* !refl_phomotopy_hconcat ⬝ (idp ◾hp* !refl_symm ⬝ !hconcat_phomotopy_rfl)⁻¹ ◾h* idp
+  end
+
+  definition hconcat_phomotopy_hconcat_cancel (p : psquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (q : f₂₁' ~* f₂₁) (r : psquare f₃₀ f₃₂ f₂₁ f₄₁) : (p ⬝hp* q) ⬝h* (q ⬝ph* r) = p ⬝h* r :=
+  begin
+    induction q using phomotopy_rec_idp,
+    exact !hconcat_phomotopy_rfl ◾h* !refl_phomotopy_hconcat
+  end
+
+  definition phomotopy_hconcat_phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂}
+    (p : f₀₁' ~* f₀₁) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : (p ⬝ph* q)⁻¹ʰ* = q⁻¹ʰ* ⬝hp* p :=
+  begin
+    induction p using phomotopy_rec_idp,
+    exact !refl_phomotopy_hconcat⁻²ʰ* ⬝ !hconcat_phomotopy_rfl⁻¹
+  end
+
+  definition hconcat_phomotopy_phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂}
+    (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) : (p ⬝hp* q)⁻¹ʰ* = q ⬝ph* p⁻¹ʰ* :=
+  begin
+    induction q using phomotopy_rec_idp,
+    exact !hconcat_phomotopy_rfl⁻²ʰ* ⬝ !refl_phomotopy_hconcat⁻¹
+  end
+
+  definition pvconst_square_phinverse (f₁₀ : A₀₀ ≃* A₂₀) (f₁₂ : A₀₂ ≃* A₂₂) :
+    (pvconst_square f₁₀ f₁₂)⁻¹ʰ* = pvconst_square f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* :=
+  begin
+    exact sorry
+  end
+
+  definition ppcompose_left_phomotopy_hconcat (A : Type*) (p : f₀₁' ~* f₀₁)
+    (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : ppcompose_left_psquare (p ⬝ph* q) =
+    @ppcompose_left_phomotopy A _ _ _ _ p ⬝ph* ppcompose_left_psquare q :=
+  sorry --used
+
+  definition ppcompose_left_hconcat_phomotopy (A : Type*) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (q : f₂₁' ~* f₂₁) : ppcompose_left_psquare (p ⬝hp* q) =
+    ppcompose_left_psquare p ⬝hp* @ppcompose_left_phomotopy A _ _ _ _ q :=
+  sorry
+
+  definition ppcompose_left_pvconst_square (A : Type*) (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) :
+    ppcompose_left_psquare (pvconst_square f₁₀ f₁₂) =
+    !ppcompose_left_pconst ⬝ph* pvconst_square (ppcompose_left f₁₀) (@ppcompose_left A _ _ f₁₂) ⬝hp*
+    !ppcompose_left_pconst :=
   sorry
 
   end psquare
@@ -282,6 +509,72 @@ namespace pointed
     A →* pointed.MK B (f pt) :=
   pmap.mk f idp
 
+  definition papply_natural_right [constructor] {A B B' : Type*} (f : B →* B') (a : A) :
+    psquare (papply B a) (papply B' a) (ppcompose_left f) f :=
+  begin
+    fapply phomotopy.mk,
+    { intro g, reflexivity },
+    { refine !idp_con ⬝ !ap_eq_of_phomotopy ⬝ !idp_con⁻¹ }
+  end
+
+  -- definition foo {A B : Type} {f : A → B} {a₀ a₁ a₂ : A} {b₀ b₁ b₂ : B}
+  --   {p₀ : a₀ = a₀} {p₁ : a₀ = a₀} (q₀ : ap f p₀ = idp) (q₁ : ap f p₁ = idp) :
+  --   whisker_right (ap f p₁) (idp_con (ap f p₀⁻¹) ⬝ !ap_inv ⬝ q₀⁻²)⁻¹ ⬝ !con.assoc ⬝
+  --   whisker_left idp (con_eq_of_eq_con_inv (eq_con_inv_of_con_eq _)) ⬝ _
+  --   = !idp_con ⬝ q₁ :=
+  -- _
+
+/-
+whisker_right
+    (ap (λ f, pppi.to_fun f a)
+       (eq_of_phomotopy (pcompose_pconst (pconst B B'))))
+    (idp_con
+       (ap (λ y, pppi.to_fun y a)
+          (eq_of_phomotopy
+             (pconst_pcompose (ppi_const (λ a, B))))⁻¹) ⬝ ap_inv
+       (λ y, pppi.to_fun y a)
+       (eq_of_phomotopy
+          (pconst_pcompose (ppi_const (λ a, B)))) ⬝ inverse2
+       (ap_eq_of_phomotopy (pconst_pcompose (ppi_const (λ a, B)))
+          a))⁻¹ ⬝ (con.assoc
+     (ppi.to_fun (pvconst_square (papply B a) (papply B' a))
+        (ppi_const (λ a, B)))
+     (ap (λ f, pppi.to_fun f a)
+        (eq_of_phomotopy (pconst_pcompose (ppi_const (λ a, B))))⁻¹)
+     (ap (λ f, pppi.to_fun f a)
+        (eq_of_phomotopy
+           (pcompose_pconst (pconst B B')))) ⬝ whisker_left
+     (ppi.to_fun (pvconst_square (papply B a) (papply B' a))
+        (ppi_const (λ a, B)))
+     (con_eq_of_eq_con_inv
+        (eq_con_inv_of_con_eq
+           (pwhisker_left_1 B' (ppmap A B) (ppmap A B') (papply B' a)
+              (pconst (ppmap A B) (ppmap A B'))
+              (ppcompose_left (pconst B B'))
+              (ppcompose_left_pconst A B B')⁻¹*))) ⬝ respect_pt
+     (pvconst_square (papply B a) (papply B' a))) = idp_con
+    (ap (λ f, pppi.to_fun f a)
+       (eq_of_phomotopy
+          (pcompose_pconst (pconst B B')))) ⬝ ap_eq_of_phomotopy
+    (pcompose_pconst (pconst B B'))
+    a
+-/
+
+
+
+  definition papply_natural_right_pconst {A : Type*} (B B' : Type*) (a : A) :
+    papply_natural_right (pconst B B') a = !ppcompose_left_pconst ⬝ph* !pvconst_square :=
+  begin
+    fapply phomotopy_mk_eq,
+    { intro g, symmetry, refine !idp_con ⬝ !ap_inv ⬝ !ap_eq_of_phomotopy⁻² },
+    {
+
+      esimp [pvconst_square],
+    --esimp [inv_con_eq_of_eq_con, pwhisker_left_1]
+      exact sorry }
+  end
+
+
   /- TODO: computation rule -/
   open pi
   definition fiberwise_pointed_map_rec {A : Type} {B : A → Type*}

spectrum/basic.hlean

@@ -749,7 +749,7 @@ namespace spectrum
     begin
       intro k,
       note sq1 := homotopy_group_homomorphism_psquare (k+2) (ptranspose (smap.glue_square f (-n - 2 +[ℤ] k))),
-      note sq2 := homotopy_group_functor_hsquare (k+2) (ap1_psquare (ptransport_natural E F f (add.assoc (-n - 2) k 1))),
+      note sq2 := homotopy_group_functor_psquare (k+2) (ap1_psquare (ptransport_natural E F f (add.assoc (-n - 2) k 1))),
       note sq3 := (homotopy_group_succ_in_natural (k+2) (f (-n - 2 +[ℤ] (k+1))))⁻¹ʰᵗʸʰ,
       note sq4 := hsquare_of_psquare sq2,
       note rect := sq1 ⬝htyh sq4 ⬝htyh sq3,

spectrum/smash.hlean

@@ -14,7 +14,8 @@ prespectrum.mk (λ z, X ∧ Y z) begin
   exact !glue
 end
 
-definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* X') (g : Y →ₛ Y') : smash_prespectrum X Y →ₛ smash_prespectrum X' Y' :=
+definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* X') (g : Y →ₛ Y') :
+  smash_prespectrum X Y →ₛ smash_prespectrum X' Y' :=
 smap.mk (λn, smash_functor f (g n)) begin
   intro n,
   refine susp_to_loop_psquare _ _ _ _ _,
@@ -22,12 +23,12 @@ smap.mk (λn, smash_functor f (g n)) begin
   refine vconcat_phomotopy _ (smash_functor_split f (g (S n))),
   refine phomotopy_vconcat (smash_functor_split f (susp_functor (g n))) _,
   refine phconcat _ _,
-  let glue_adjoint := susp_pelim (Y n) (Y (S n)) (glue Y n),
+  let glue_adjoint := susp_pelim (Y' n) (Y' (S n)) (glue Y' n),
-  exact pid X' ∧→ glue_adjoint,
+  exact pid X ∧→ glue_adjoint,
-  exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint),
+  refine smash_functor_psquare (phrefl (pid X)) _,
-  refine smash_functor_psquare (phrefl (pid X')) _,
   refine loop_to_susp_square _ _ _ _ _,
-  exact smap.glue_square g n
+  exact smap.glue_square g n,
+  exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint)
 end
 
   /- smash of a spectrum and a type -/