From e6310ed3894616bf1f30c1868535ab281d75d854 Mon Sep 17 00:00:00 2001
From: PHart3 <perry.hart7@yahoo.com>
Date: Sun, 15 Dec 2024 11:46:00 -0600
Subject: [PATCH] finished 2-coherence proof

---
 Colimit-code/Aux/Coslice.agda        |  6 +--
 Colimit-code/Trunc-Cos/TruncAdj.agda | 72 ++++++++++++++++++++++++----
 2 files changed, 65 insertions(+), 13 deletions(-)

diff --git a/Colimit-code/Aux/Coslice.agda b/Colimit-code/Aux/Coslice.agda
index e168599..833e9cb 100644
--- a/Colimit-code/Aux/Coslice.agda
+++ b/Colimit-code/Aux/Coslice.agda
@@ -78,11 +78,11 @@ module MapsCos {j : ULevel} (A : Type j) where
     ap (λ p → ap (fst h₂) (snd f a) ∙ p) (snd H a)
 
   -- concatenation
-  infixr 40 <_>_∼∘_
-  <_>_∼∘_ : ∀ {i k} (X : Coslice i j A) {Y : Coslice k j A} →
+  infixr 40 _∼∘-cos_
+  _∼∘-cos_ : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} →
     {h₁ h₂ h₃ : X *→ Y} →
     < X > h₁ ∼ h₂ → < X > h₂ ∼ h₃ → < X > h₁ ∼ h₃
-  <_>_∼∘_ X {h₁ = h₁} (H₁ , H₂) (K₁ , K₂) =
+  _∼∘-cos_ {X = X} {h₁ = h₁} (H₁ , H₂) (K₁ , K₂) =
     (λ x → H₁ x ∙ K₁ x) ,
     (λ a →
       (ap (λ p → p ∙ snd h₁ a) (!-∙ (H₁ (fun X a)) (K₁ (fun X a))) ∙
diff --git a/Colimit-code/Trunc-Cos/TruncAdj.agda b/Colimit-code/Trunc-Cos/TruncAdj.agda
index 1f149b2..104e55c 100644
--- a/Colimit-code/Trunc-Cos/TruncAdj.agda
+++ b/Colimit-code/Trunc-Cos/TruncAdj.agda
@@ -32,24 +32,76 @@ module _ {j} (A : Type j) where
 
     -- hom map of the adjunction
     Trunc-cos-hom : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A}
-      {{p : has-level n (ty Y)}} → (X *→ Y) → (Trunc-cos X *→ Y)
-    fst (Trunc-cos-hom f) = Trunc-rec (fst f)
+      {{p : has-level n (ty Y)}} → (Trunc-cos X *→ Y) → (X *→ Y)
+    fst (Trunc-cos-hom f) = fst f ∘ [_]
     snd (Trunc-cos-hom f) a = snd f a
 
     -- naturality of hom map
     Trunc-cos-∘-nat : ∀ {i k ℓ} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice ℓ j A}
-      {{p : has-level n (ty Y)}} (f : Z *→ X) (h : X *→ Y)
-      → < Trunc-cos Z > Trunc-cos-hom h ∘* Trunc-cos-fmap f ∼ Trunc-cos-hom (h ∘* f) 
-    fst (Trunc-cos-∘-nat f h) = Trunc-elim (λ _ → idp)
-    snd (Trunc-cos-∘-nat f h) a = ap (λ p → p ∙ snd h a) (∘-ap (Trunc-elim (fst h)) [_] (snd f a))
+      {{p : has-level n (ty Y)}} (f : Z *→ X) (h : Trunc-cos X *→ Y)
+      → < Z > Trunc-cos-hom h ∘* f ∼ Trunc-cos-hom (h ∘* Trunc-cos-fmap f) 
+    fst (Trunc-cos-∘-nat f h) x = idp
+    snd (Trunc-cos-∘-nat f h) a = ap (λ p → p ∙ snd h a) (ap-∘ (fst h) [_] (snd f a))
 
     ap-Trunc-cos-hom : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} {{p : has-level n (ty Y)}}
-      {h₁ h₂ : X *→ Y} → < X > h₁ ∼ h₂ → < Trunc-cos X > Trunc-cos-hom h₁ ∼ Trunc-cos-hom h₂
-    fst (ap-Trunc-cos-hom H) = Trunc-elim (λ x → fst H x)
+      {h₁ h₂ : Trunc-cos X *→ Y} → < Trunc-cos X > h₁ ∼ h₂ → < X > Trunc-cos-hom h₁ ∼ Trunc-cos-hom h₂
+    fst (ap-Trunc-cos-hom H) x = fst H [ x ]
     snd (ap-Trunc-cos-hom H) a = snd H a
 
     -- Our custom ap function behaves as expected
     ap-Trunc-cos-hom-id : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} {{p : has-level n (ty Y)}}
-      (f : X *→ Y) → < Trunc-cos X > ap-Trunc-cos-hom (cos∼id f) ∼∼ cos∼id (Trunc-cos-hom f)
-    fst (ap-Trunc-cos-hom-id f) = Trunc-elim (λ _ → idp)
+      (f : Trunc-cos X *→ Y) → < X > ap-Trunc-cos-hom (cos∼id f) ∼∼ cos∼id (Trunc-cos-hom f)
+    fst (ap-Trunc-cos-hom-id f) x = idp
     snd (ap-Trunc-cos-hom-id f) a = idp
+
+    -- Truncation on coslices is a 2-coherent left adjoint
+
+    module _ {i₁ i₂ i₃ i₄}
+      {X : Coslice i₁ j A} {Y : Coslice i₂ j A} {Z : Coslice i₃ j A} {W : Coslice i₄ j A}
+      {{p : has-level n (ty Y)}}
+      (f₂ : Z *→ X) (f₃ : W *→ Z) (f₁ : Trunc-cos X *→ Y) where
+
+      two-coher-Trunc-cos :
+        < W >
+          (pre-∘*-∼ f₃ (Trunc-cos-∘-nat f₂ f₁)) ∼∘-cos
+          Trunc-cos-∘-nat f₃ (f₁ ∘* Trunc-cos-fmap f₂) ∼∘-cos
+          ap-Trunc-cos-hom (*→-assoc f₁ (Trunc-cos-fmap f₂) (Trunc-cos-fmap f₃))
+        ∼∼
+          *→-assoc (Trunc-cos-hom f₁) f₂ f₃ ∼∘-cos
+          Trunc-cos-∘-nat (f₂ ∘* f₃) f₁ ∼∘-cos
+          ap-Trunc-cos-hom (post-∘*-∼ f₁ (Trunc-cos-fmap-∘ f₂ f₃))
+      fst two-coher-Trunc-cos x = idp
+      snd two-coher-Trunc-cos a = lemma a (snd f₃ a)
+        where
+          lemma : (a : A) {w : ty Z} (τ : w == fun Z a) → 
+            ap (λ q → q) ((ap (λ p₁ → p₁ ∙ ap (λ x → fst f₁ [ x ])
+              (snd f₂ a) ∙ snd f₁ a)
+              (hmtpy-nat-!-sq (λ x → idp) τ) ∙
+              ∙-assoc (ap (λ z → fst f₁ [ fst f₂ z ]) τ) idp
+              (ap (λ x → fst f₁ [ x ]) (snd f₂ a) ∙ snd f₁ a)) ∙
+              ap (_∙_ (ap (λ z → fst f₁ [ fst f₂ z ]) τ))
+              (ap (λ p₁ → p₁ ∙ snd f₁ a) (ap-∘ (fst f₁) [_] (snd f₂ a)))) ∙
+            ap (λ q → q) (ap (λ p₁ → p₁ ∙ ap (fst f₁)
+              (ap [_] (snd f₂ a)) ∙ snd f₁ a)
+              (ap-∘ (λ x → fst f₁ (Trunc-elim (λ x₁ → [ fst f₂ x₁ ]) x))
+              [_] τ)) ∙
+            ap (λ p₁ → p₁ ∙ ap (fst f₁) (ap [_] (snd f₂ a)) ∙ snd f₁ a)
+              (ap-∘ (fst f₁) (Trunc-elim (λ x → [ fst f₂ x ]))
+              (ap [_] τ)) ∙
+            ! (ap2-∙-∙ (fst f₁) (Trunc-elim (λ x → [ fst f₂ x ]))
+              (ap [_] τ) (ap [_] (snd f₂ a)) (snd f₁ a))
+            ==
+            ap (λ q → q) (ap (λ p₁ → p₁ ∙ ap (λ x → fst f₁ [ x ])
+              (snd f₂ a) ∙ snd f₁ a)
+              (ap-∘ (λ x → fst f₁ [ x ]) (fst f₂) τ) ∙
+              ! (ap2-∙-∙ (λ x → fst f₁ [ x ]) (fst f₂) τ
+              (snd f₂ a) (snd f₁ a))) ∙
+            ap (λ q → q) (ap (λ p₁ → p₁ ∙ snd f₁ a)
+              (ap-∘ (fst f₁) [_] (ap (fst f₂) τ ∙ snd f₂ a))) ∙
+            ap (λ p₁ → ap (fst f₁) p₁ ∙ snd f₁ a)
+              (ap-∘-∙ [_] (fst f₂) τ (snd f₂ a) ∙
+              ap (λ p₁ → p₁ ∙ ap [_] (snd f₂ a))
+              (ap-∘ (Trunc-elim (λ x → [ fst f₂ x ])) [_] τ))
+          lemma a idp =
+            ap (λ p → p ∙ idp) (ap-idf (ap (λ q → q)
+              (ap (λ p₁ → p₁ ∙ snd f₁ a) (ap-∘ (fst f₁) [_] (snd f₂ a)))))