higher groups: prove naturality of all adjunctions

higher_groups.hlean

@@ -149,12 +149,12 @@ definition Decat_adjoint_Disc (G : [n+1;k]Grp) (H : [n;k]Grp) :
 pmap_ptrunc_pequiv (n + k) (B G) (B H)
 
 definition Decat_adjoint_Disc_natural {G G' : [n+1;k]Grp} {H H' : [n;k]Grp}
-  (eG : B G' ≃* B G) (eH : B H ≃* B H') :
+  (g : B G' →* B G) (h : B H →* B H') :
   psquare (Decat_adjoint_Disc G H)
           (Decat_adjoint_Disc G' H')
-          (ppcompose_left eH ∘* ppcompose_right (ptrunc_functor _ eG))
-          (ppcompose_left eH ∘* ppcompose_right eG) :=
-sorry
+          (ppcompose_left h ∘* ppcompose_right (ptrunc_functor _ g))
+          (ppcompose_left h ∘* ppcompose_right g) :=
+pmap_ptrunc_pequiv_natural (n + k) g h
 
 definition Decat_Disc (G : [n;k]Grp) : Decat (Disc G) = G :=
 Grp_eq !ptrunc_pequiv
@@ -195,6 +195,14 @@ definition Deloop_adjoint_Loop (G : [n;k+1]Grp) (H : [n+1;k]Grp) :
   ppmap (B (Deloop G)) (B H) ≃* ppmap (B G) (B (Loop H)) :=
 (connect_intro_pequiv _ !is_conn_pconntype)⁻¹ᵉ*
 
+definition Deloop_adjoint_Loop_natural {G G' : [n;k+1]Grp} {H H' : [n+1;k]Grp}
+  (g : B G' →* B G) (h : B H →* B H') :
+  psquare (Deloop_adjoint_Loop G H)
+          (Deloop_adjoint_Loop G' H')
+          (ppcompose_left h ∘* ppcompose_right g)
+          (ppcompose_left (connect_functor k h) ∘* ppcompose_right g) :=
+(connect_intro_pequiv_natural g h _ _)⁻¹ʰ*
+
 /- to do: naturality -/
 
 definition Loop_Deloop (G : [n;k+1]Grp) : Loop (Deloop G) = G :=
@@ -223,6 +231,19 @@ definition Stabilize_adjoint_Forget (G : [n;k]Grp) (H : [n;k+1]Grp) :
 have is_trunc (n + k + 1) (B H), from !is_trunc_B,
 pmap_ptrunc_pequiv (n + k + 1) (⅀ (B G)) (B H) ⬝e* susp_adjoint_loop (B G) (B H)
 
+definition Stabilize_adjoint_Forget_natural {G G' : [n;k]Grp} {H H' : [n;k+1]Grp}
+  (g : B G' →* B G) (h : B H →* B H') :
+  psquare (Stabilize_adjoint_Forget G H)
+          (Stabilize_adjoint_Forget G' H')
+          (ppcompose_left h ∘* ppcompose_right (ptrunc_functor (n+k+1) (⅀→ g)))
+          (ppcompose_left (Ω→ h) ∘* ppcompose_right g) :=
+begin
+  have is_trunc (n + k + 1) (B H), from !is_trunc_B,
+  have is_trunc (n + k + 1) (B H'), from !is_trunc_B,
+  refine pmap_ptrunc_pequiv_natural (n+k+1) (⅀→ g) h ⬝h* _,
+  exact susp_adjoint_loop_natural_left g ⬝v* susp_adjoint_loop_natural_right h
+end
+
 /- to do: naturality -/
 
 definition ωForget (k : ℕ) (G : [n;ω]Grp) : [n;k]Grp :=
@@ -348,14 +369,15 @@ sorry
 
 --has sorry
 print axioms ωstabilization
-print axioms Decat_adjoint_Disc_natural
 print axioms cGrp_equivalence_Grp
 
-
 -- no sorry's
 print axioms Decat_adjoint_Disc
+print axioms Decat_adjoint_Disc_natural
 print axioms Deloop_adjoint_Loop
+print axioms Deloop_adjoint_Loop_natural
 print axioms Stabilize_adjoint_Forget
+print axioms Stabilize_adjoint_Forget_natural
 print axioms stabilization
 print axioms is_trunc_Grp
 

move_to_lib.hlean

@@ -1129,6 +1129,33 @@ pmap.mk (fiber_functor g h H (respect_pt h))
       exact !con.assoc ⬝ to_homotopy_pt H
   end
 
+definition ppoint_natural {A A' B B' : Type*} {f : A →* B} {f' : A' →* B'}
+  (g : A →* A') (h : B →* B') (H : psquare g h f f') :
+  psquare (ppoint f) (ppoint f') (pfiber_functor g h H) g :=
+begin
+  fapply phomotopy.mk,
+  { intro x, reflexivity },
+  { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, esimp, apply point_fiber_eq }
+end
+
+/- if we need this: do pfiber_functor_pcompose and so on first -/
+-- definition psquare_pfiber_functor [constructor] {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Type*}
+--   {f₁ : A₁ →* B₁} {f₂ : A₂ →* B₂} {f₃ : A₃ →* B₃} {f₄ : A₄ →* B₄}
+--   {g₁₂ : A₁ →* A₂} {g₃₄ : A₃ →* A₄} {g₁₃ : A₁ →* A₃} {g₂₄ : A₂ →* A₄}
+--   {h₁₂ : B₁ →* B₂} {h₃₄ : B₃ →* B₄} {h₁₃ : B₁ →* B₃} {h₂₄ : B₂ →* B₄}
+--   (H₁₂ : psquare g₁₂ h₁₂ f₁ f₂) (H₃₄ : psquare g₃₄ h₃₄ f₃ f₄)
+--   (H₁₃ : psquare g₁₃ h₁₃ f₁ f₃) (H₂₄ : psquare g₂₄ h₂₄ f₂ f₄)
+--   (G : psquare g₁₂ g₃₄ g₁₃ g₂₄) (H : psquare h₁₂ h₃₄ h₁₃ h₂₄)
+--   /- pcube H₁₂ H₃₄ H₁₃ H₂₄ G H -/ :
+--   psquare (pfiber_functor g₁₂ h₁₂ H₁₂) (pfiber_functor g₃₄ h₃₄ H₃₄)
+--           (pfiber_functor g₁₃ h₁₃ H₁₃) (pfiber_functor g₂₄ h₂₄ H₂₄) :=
+-- begin
+--   fapply phomotopy.mk,
+--   { intro x, induction x with x p, induction B₁ with B₁ b₁₀, induction f₁ with f₁ f₁₀, esimp at *,
+--     induction p, esimp [fiber_functor], },
+--   { }
+-- end
+
 -- TODO: use this in pfiber_pequiv_of_phomotopy
 definition fiber_equiv_of_homotopy {A B : Type} {f g : A → B} (h : f ~ g) (b : B)
   : fiber f b ≃ fiber g b :=
@@ -1361,7 +1388,7 @@ definition connect_intro_equiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (
   (X →* connect k Y) ≃ (X →* Y) :=
 begin
   fapply equiv.MK,
-  { intro f, exact ppoint (ptr k Y) ∘* f },
+  { intro f, exact ppoint (ptr k Y) ∘*  f },
   { intro g, exact connect_intro H g },
   { intro g, apply eq_of_phomotopy, exact ppoint_connect_intro H g },
   { intro f, apply eq_of_phomotopy, exact connect_intro_ppoint H f }
@@ -1386,6 +1413,31 @@ loopn_pfiber (k+1) (ptr k X) ⬝e*
 definition is_conn_of_is_conn_succ_nat (n : ℕ) (A : Type) [is_conn (n+1) A] : is_conn n A :=
 is_conn_of_is_conn_succ n A
 
+definition connect_functor (k : ℕ) {X Y : Type*} (f : X →* Y) : connect k X →* connect k Y :=
+pfiber_functor f (ptrunc_functor k f) (ptr_natural k f)⁻¹*
+
+definition connect_intro_pequiv_natural {k : ℕ} {X X' : Type*} {Y Y' : Type*} (f : X' →* X)
+  (g : Y →* Y') (H : is_conn k X) (H' : is_conn k X') :
+  psquare (connect_intro_pequiv Y H) (connect_intro_pequiv Y' H')
+          (ppcompose_left (connect_functor k g) ∘* ppcompose_right f)
+          (ppcompose_left g ∘* ppcompose_right f) :=
+begin
+  refine _ ⬝v* _, exact connect_intro_pequiv Y H',
+  { fapply phomotopy.mk,
+    { intro h, apply eq_of_phomotopy, apply passoc },
+    { xrewrite [▸*, pcompose_right_eq_of_phomotopy, pcompose_left_eq_of_phomotopy,
+        -+eq_of_phomotopy_trans],
+      apply ap eq_of_phomotopy, apply passoc_pconst_middle }},
+  { fapply phomotopy.mk,
+    { intro h, apply eq_of_phomotopy,
+      refine !passoc⁻¹* ⬝* pwhisker_right h (ppoint_natural _ _ _) ⬝* !passoc },
+    { xrewrite [▸*, +pcompose_left_eq_of_phomotopy, -+eq_of_phomotopy_trans],
+      apply ap eq_of_phomotopy,
+      refine !trans_assoc ⬝ idp ◾** !passoc_pconst_right ⬝ _,
+      refine !trans_assoc ⬝ idp ◾** !pcompose_pconst_phomotopy ⬝ _,
+      apply symm_trans_eq_of_eq_trans, symmetry, apply passoc_pconst_right }}
+end
+
 end is_conn
 
 namespace misc

pointed.hlean

@@ -202,6 +202,15 @@ namespace pointed
   -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q :=
   -- sorry
 
+  definition pconst_pcompose_phomotopy {A B C : Type*} {f f' : A →* B} (p : f ~* f') :
+    pwhisker_left (pconst B C) p ⬝* pconst_pcompose f' = pconst_pcompose f :=
+  begin
+    fapply phomotopy_eq,
+    { intro a, apply ap_constant },
+    { induction p using phomotopy_rec_idp, induction B with B b₀, induction f with f f₀,
+      esimp at *, induction f₀, reflexivity }
+  end
+
 /- Homotopy between a function and its eta expansion -/
 
   definition pmap_eta [constructor] {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) :=

pointed_pi.hlean

@@ -940,3 +940,33 @@ namespace is_conn
   end
 
 end is_conn
+
+
+/- TODO: move, these facts use some of these pointed properties -/
+
+namespace trunc
+
+lemma pmap_ptrunc_pequiv_natural [constructor] (n : ℕ₋₂) {A A' B B' : Type*}
+  [H : is_trunc n B] [H : is_trunc n B'] (f : A' →* A) (g : B →* B') :
+  psquare (pmap_ptrunc_pequiv n A B) (pmap_ptrunc_pequiv n A' B')
+          (ppcompose_left g ∘* ppcompose_right (ptrunc_functor n f))
+          (ppcompose_left g ∘* ppcompose_right f) :=
+begin
+  refine _ ⬝v* _, exact pmap_ptrunc_pequiv n A' B,
+  { fapply phomotopy.mk,
+    { intro h, apply eq_of_phomotopy,
+      exact !passoc ⬝* pwhisker_left h (ptr_natural n f)⁻¹* ⬝* !passoc⁻¹* },
+    { xrewrite [▸*, +pcompose_right_eq_of_phomotopy, -+eq_of_phomotopy_trans],
+      apply ap eq_of_phomotopy,
+      refine !trans_assoc ⬝ idp ◾** (!trans_assoc⁻¹ ⬝ (eq_bot_of_phsquare (phtranspose
+               (passoc_pconst_left (ptrunc_functor n f) (ptr n A'))))⁻¹) ⬝ _,
+      refine !trans_assoc ⬝ idp ◾** !pconst_pcompose_phomotopy ⬝ _,
+      apply passoc_pconst_left }},
+  { fapply phomotopy.mk,
+    { intro h, apply eq_of_phomotopy, exact !passoc⁻¹* },
+    { xrewrite [▸*, pcompose_right_eq_of_phomotopy, pcompose_left_eq_of_phomotopy,
+        -+eq_of_phomotopy_trans],
+      apply ap eq_of_phomotopy, apply symm_trans_eq_of_eq_trans, symmetry,
+      apply passoc_pconst_middle }}
+end
+end trunc