2-coherence of truncation, newer Agda version, etc. (#9)

* first commit

* adding basic A-homotopy operations

* adding truncation functor on coslices

* finished 2-coherence proof

* update Dockerfile

* update to Agda 2.6.4.3

* define ptd homotopy via == instead of =-=

* new name for helper function

* fix function name

Colimit-code/Aux/Coslice.agda

@@ -29,9 +29,9 @@ infixr 40 <_>_∘_
 
 infixr 30 [_,_]_∼_
 [_,_]_∼_ :  ∀ {i j k} (A : Type j) (X : Coslice i j A) {Y : Coslice k j A} →
-  < A >  X *→ Y  →  < A >  X *→ Y →  Type (lmax (lmax i k) j)    
+  < A > X *→ Y → < A > X *→ Y → Type (lmax (lmax i k) j)    
 [ A , *[ X , f ] ] ( h₁ , p₁ )∼( h₂ , p₂ ) = Σ ((x : X) → h₁ x == h₂ x)
-  (λ H → ((a : A) →  (! (H (f a)) ∙ (p₁ a) == p₂ a) ))
+  (λ H → ((a : A) →  (! (H (f a)) ∙ (p₁ a) == p₂ a)))
 
 module MapsCos {j : ULevel} (A : Type j) where
 
@@ -46,5 +46,59 @@ module MapsCos {j : ULevel} (A : Type j) where
 
   infixr 30 <_>_∼_
   <_>_∼_ : ∀ {i k} (X : Coslice i j A) {Y : Coslice k j A} →
-    < A >  X *→ Y  →  < A >  X *→ Y →  Type (lmax (lmax i k) j)    
+    X *→ Y →  X *→ Y → Type (lmax (lmax i k) j)    
   < X > h ∼ g = [ A , X ] h ∼ g 
+
+  *→-assoc : ∀ {i k l ℓ} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice l j A}
+    {W : Coslice ℓ j A} (h₃ : Z *→ W) (h₂ : Y *→ Z) (h₁ : X *→ Y) →
+    < X > (h₃ ∘* h₂) ∘* h₁ ∼ h₃ ∘* (h₂ ∘* h₁)
+  fst (*→-assoc h₃ h₂ h₁) x = idp
+  snd (*→-assoc h₃ h₂ h₁) a =
+    ap (λ p → p ∙ ap (fst h₃) (snd h₂ a) ∙ snd h₃ a) (ap-∘ (fst h₃) (fst h₂) (snd h₁ a)) ∙
+    ! (ap2-∙-∙ (fst h₃) (fst h₂) (snd h₁ a) (snd h₂ a) (snd h₃ a))
+
+  -- post-composition
+  post-∘*-∼ : ∀ {i k l} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice l j A}
+    {h₁ h₂ : X *→ Y} (f : Y *→ Z) → < X > h₁ ∼ h₂ → < X > f ∘* h₁ ∼ f ∘* h₂ 
+  fst (post-∘*-∼ f H) x = ap (fst f) (fst H x)
+  snd (post-∘*-∼ {X = X} {h₁ = h₁} f H) a = 
+    ap (λ p → p ∙ ap (fst f) (snd h₁ a) ∙ snd f a) (!-ap (fst f) (fst H (fun X a))) ∙ 
+    ! (∙-assoc (ap (fst f) (! (fst H (fun X a)))) (ap (fst f) (snd h₁ a)) (snd f a)) ∙
+    ap (λ p → p ∙ snd f a) (∙-ap (fst f) (! (fst H (fun X a))) (snd h₁ a)) ∙
+    ap (λ p → ap (fst f) p ∙ snd f a) (snd H a)
+
+  -- pre-composition
+  pre-∘*-∼ : ∀ {i k l} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice l j A}
+    {h₁ h₂ : X *→ Y} (f : Z *→ X) → < X > h₁ ∼ h₂ → < Z > h₁ ∘* f ∼ h₂ ∘* f
+  fst (pre-∘*-∼ f H) x = fst H (fst f x)
+  snd (pre-∘*-∼ {X = X} {Z = Z} {h₁ = h₁} {h₂} f H) a =
+    (! (∙-assoc (! (fst H (fst f (fun Z a)))) (ap (fst h₁) (snd f a)) (snd h₁ a)) ∙
+      ap (λ p → p ∙ snd h₁ a) (hmtpy-nat-!-sq (fst H) (snd f a)) ∙
+      ∙-assoc (ap (fst h₂) (snd f a)) (! (fst H (fun X a))) (snd h₁ a)) ∙
+    ap (λ p → ap (fst h₂) (snd f a) ∙ p) (snd H a)
+
+  -- concatenation
+  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₃
+  _∼∘-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))) ∙
+      ∙-assoc (! (K₁ (fun X a))) (! (H₁ (fun X a))) (snd h₁ a)) ∙
+      ap (λ p → ! (K₁ (fun X a)) ∙ p) (H₂ a) ∙ K₂ a)
+
+  -- identity
+  cos∼id : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} (h : X *→ Y)
+    → < X > h ∼ h
+  fst (cos∼id h) = λ x → idp
+  snd (cos∼id h) = λ a → idp
+
+  -- homotopy of homotopies of A-maps
+  infixr 30 <_>_∼∼_
+  <_>_∼∼_ : ∀ {i k} (X : Coslice i j A) {Y : Coslice k j A} {h₁ h₂ : X *→ Y} →
+    < X > h₁ ∼ h₂ → < X > h₁ ∼ h₂ → Type (lmax k (lmax i j))
+  <_>_∼∼_ X {h₁ = h₁} H₁ H₂ =
+    Σ (fst H₁ ∼ fst H₂)
+      λ K → (a : A) → ap (λ p → ! p ∙ snd h₁ a) (! (K (fun X a))) ∙ snd H₁ a == snd H₂ a

Colimit-code/Aux/Diagram.agda

@@ -106,5 +106,5 @@ module _ {ℓi ℓj k} {A : Type ℓj} {Γ : Graph ℓv ℓe} {F : CosDiag ℓi
   PostComp : ∀ {k'} {D : Coslice k' ℓj A} → CosCocone A F C → (< A > C *→ D) →  CosCocone A F D
   comp (PostComp K (f , fₚ)) i = f ∘ (fst (comp K i)) , λ a → ap f (snd (comp K i) a) ∙ fₚ a 
   comTri (PostComp K (f , fₚ)) {y = j} {x = i} g = (λ x → ap f (fst (comTri K g) x)) ,
-    λ a →   ap-cp-revR f (fst (comp K j)) (snd (F <#> g) a)  (fst (comTri K g) (fun (F # i) a)) ∙
+    λ a → ap-cp-revR f (fst (comp K j)) (snd (F <#> g) a) (fst (comTri K g) (fun (F # i) a)) ∙
       ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri K g) a))

Colimit-code/Map-Nat/CosColimitMap18.agda

@@ -109,7 +109,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type 
         ap (λ p → ap f p ∙ idp) (ap (λ p → ! (ap right (! (ap (cin j) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) ∙ p)) ∙ idp)
           (apCommSq2 (λ x → cin j (fst (G <#> g) x)) (λ v → cin j (fst (G <#> g) v)) (λ x → idp) τ₁₀) ∙
           !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) (λ v → cin j (fst (G <#> g) v)) right τ₁₀ τ₁₃ idp idp idp ∙ idp)) ∙
-        ap-∘-∙ f (right ∘ (λ v → cin j (fst (G <#> g) v))) τ₁₀ (ap (right ∘ cin j) τ₁₃ ∙ idp)
+        ap-∘-∙-∙ f (right ∘ (λ v → cin j (fst (G <#> g) v))) τ₁₀ (ap (right ∘ cin j) τ₁₃ ∙ idp)
           ==
         !-!-∙-pth (ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) idp ∙
         ap (λ p → p ∙ ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp) ∙ idp) (hmtpy-nat-! (λ x → idp) τ₁₀) ∙
@@ -145,7 +145,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type 
           (apCommSq2 (λ x → cin j (fst (G <#> g) x)) (cin i) (cglue g) τ₁₀) ∙
           !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) (cin i) right τ₁₀ τ₁₃ idp
           idp (cglue g (fun (G # i) a)) ∙ idp)) ∙
-        ap-∘-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp)
+        ap-∘-∙-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp)
           ==
         !-!-∙-pth (ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp))
           (ap f (ap right (cglue g (fst (nat δ i) (fun (F # i) a))))) ∙
@@ -169,7 +169,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type 
           (apCommSq2 (λ x → cin j (fst (G <#> g) x)) h H τ₁₀) ∙
           !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) h right τ₁₀ τ₁₃ idp
           idp (H (fun (G # i) a)) ∙ idp)) ∙
-        ap-∘-∙ f (right ∘ h) τ₁₀ (! (ap right (H (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp)
+        ap-∘-∙-∙ f (right ∘ h) τ₁₀ (! (ap right (H (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp)
           ==
         !-!-∙-pth (ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp))
           (ap f (ap right (H (fst (nat δ i) (fun (F # i) a))))) ∙
@@ -197,7 +197,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type 
           ap (λ p → ! (ap right (! (ap (cin j) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) ∙ p)) ∙ idp)
           (apCommSq2 (λ x → cin j (fst (G <#> g) x)) (cin i) (cglue g) τ₁₀) ∙
           !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) (cin i) right τ₁₀ τ₁₃ idp idp (cglue g (fun (G # i) a)) ∙ idp)) ∙
-        ap-∘-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙
+        ap-∘-∙-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙
         ap (right ∘ cin j) τ₁₃ ∙ idp)
           ==
         !-!-∙-pth (ap (λ x → f (right (cin j x))) σ₁)
@@ -240,7 +240,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type 
           (cglue g (fst (nat δ i) (fun (F # i) a))))) ∙ idp) ∙
           ap (f ∘ right ∘ cin j ∘ fst (nat δ j)) τ₅ ∙
           ap (f ∘ right ∘ cin j) τ₆ ∙ ap f τ₇ ∙ τ₈)
-          (ap-∘-∙ f (right ∘ cin j) τ₆ τ₇) ◃∙
+          (ap-∘-∙-∙ f (right ∘ cin j) τ₆ τ₇) ◃∙
         long-path-red τ₅
           (ap (f ∘ right ∘ cin j) τ₆ ∙ ap f τ₇ ∙ τ₈)
           (ap f (ap (λ x → right (cin j x)) τ₆ ∙
@@ -264,7 +264,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type 
              right τ₁₀ τ₁₃ τ₅
              τ₆ (cglue g (fun (G # i) a)) τ₇ ∙
            ap (_∙_ (ap (λ x → right (cin i x)) τ₁₀)) τ₁)) ◃∙
-           ap-∘-∙ f (right ∘ cin i) τ₁₀ τ₁₁ ◃∎
+           ap-∘-∙-∙ f (right ∘ cin i) τ₁₀ τ₁₁ ◃∎
           =ₛ
         (!-!-∙-pth (ap (λ x → f (right (cin j x))) (comSq δ g (fun (F # i) a)))
           (ap f (ap right (cglue g (fst (nat δ i) (fun (F # i) a))))) ∙
@@ -309,7 +309,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type 
 
     CosColim-NatSq2 : CosCocEq F T (Map-to-Lim-map F (f , fₚ) K-diag) (Diag-to-Lim-map (PostComp ColCoC (f , fₚ)))
     W CosColim-NatSq2 i x = idp
-    u CosColim-NatSq2 i a = ap-∘-∙ f (right ∘ cin i) (snd (nat δ i) a) (! (glue (cin i a)))
+    u CosColim-NatSq2 i a = ap-∘-∙-∙ f (right ∘ cin i) (snd (nat δ i) a) (! (glue (cin i a)))
     Λ CosColim-NatSq2 {i} {j} g = (λ x → ap-∘-∘-!-∙-rid f right (cin j) (comSq δ g x) (cglue g (fst (nat δ i) x))) ,
       λ a → NatSq2-Λ-coher g a (snd (F <#> g) a) (snd (nat δ j) a) (! (glue (cin j a))) (fₚ a) (snd (nat δ i) a)
         (snd (G <#> g) a) (comSq-coher δ g a)

Colimit-code/Map-Nat/CosColimitPstCmp.agda

@@ -14,9 +14,9 @@ module CosColimitPstCmp where
 
 module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} (h : B → C) (f : A → B) where 
 
-  ap-∘-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c} 
+  ap-∘-∙-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c} 
     → ap h (ap f p₁ ∙ p₂) ∙ s == ap (h ∘ f) p₁ ∙ ap h p₂ ∙ s
-  ap-∘-∙ idp p₂ = idp
+  ap-∘-∙-∙ idp p₂ = idp
 
   ap-∘-rid : {x y : A} (p : x == y) → ap h (ap f p) ∙ idp == ap (h ∘ f) p
   ap-∘-rid idp = idp
@@ -71,7 +71,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
           ap φ₁ (ap f p₁) ∙ idp) ∙
           ap (φ₁ ∘ f ∘ right ∘ cin j) p₂ ∙
           ap (φ₁ ∘ f) p₃ ∙ ap φ₁ p₄ ∙ p₅))
-          (ap-∘-∙ φ₁ f p₃ p₄)  ◃∙
+          (ap-∘-∙-∙ φ₁ f p₃ p₄)  ◃∙
         long-path-red p₂
           (ap (φ₁ ∘ f) p₃ ∙
           ap φ₁ p₄ ∙ p₅)
@@ -98,7 +98,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
           ap (λ p → ap φ₁ p ∙ φ₂ a) (ap-cp-revR f (right ∘ cin j) p₂
             p₁ ∙
           ap (λ p → p ∙ fₚ a) (ap (ap f) τ))) ◃∙
-      ap-∘-∙ φ₁ f σ (fₚ a) ◃∎
+      ap-∘-∙-∙ φ₁ f σ (fₚ a) ◃∎
       =ₛ
       (ap-cp-revR (φ₁ ∘ f) (right ∘ cin j)
         p₂ p₁ ∙
@@ -107,14 +107,14 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
     NatSq-1-Λ-red2 {i} {j} g a idp idp p₃ idp = =ₛ-in (lemma p₃ (fₚ a))
       where
         lemma : {z : P} (p : right (cin j (fst (F <#> g) (fun (F # i) a))) == z) (c : f z == fun T a)
-          → ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙ φ₁ f p c == idp
+          → ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙-∙ φ₁ f p c == idp
         lemma idp c = idp
 
 -- τ = (snd (comTri ColCoC g) a)
 
     CosColim-NatSq1 : CosCocEq F U (Map-to-Lim-map (PostComp ColCoC (f , fₚ))) (PostComp ColCoC (φ ∘* (f , fₚ)))
     W CosColim-NatSq1 = λ i x → idp
-    u CosColim-NatSq1 = λ i a → ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a)  
+    u CosColim-NatSq1 = λ i a → ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a)  
     Λ CosColim-NatSq1 {i} {j} g = (λ x → ap-∘-rid φ₁ f (fst (comTri ColCoC g) x)) , λ a → lemma a
       where
         lemma : (a : A) → 
@@ -133,7 +133,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙
             ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙
             ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙
-            snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
+            snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
           long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙
             ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a)
             (ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙ -- here
@@ -143,7 +143,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
             (fst (comTri ColCoC g) (fun (F # i) a)) ∙
             ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
-          ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
+          ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
             =ₛ
           (ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j))
             (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙
@@ -165,7 +165,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙
             ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙
             ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙
-            snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
+            snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
           long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙
             ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a)
             (ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙
@@ -175,7 +175,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
             (fst (comTri ColCoC g) (fun (F # i) a)) ∙
             ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
-          ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
+          ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
             =ₛ⟨ 0 & 4 & NatSq-1-Λ-red g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a) ⟩
           ↯ (NatSq-1-Λ-aux g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a)) ◃∙ 
           ap (λ q → q) (ap-cp-revR φ₁ (f ∘ fst (comp ColCoC j)) (snd (F <#> g) a)
@@ -184,7 +184,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
             (fst (comTri ColCoC g) (fun (F # i) a)) ∙
             ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
-          ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
+          ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
             =ₛ⟨ NatSq-1-Λ-red2 g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (snd (comTri ColCoC g) a) ⟩          
           (ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j))
             (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙

Colimit-code/README.md

@@ -50,7 +50,7 @@ check the entire development in a reasonable amount of time.
 
 ## Manual Type-Checking
 
-1. Install Agda 2.6.3.
+1. Install Agda 2.6.4.3.
 2. Install the stripped, modified HoTT-Agda library under `../HoTT-Agda`.
 3. Type-check the file `Main-Theorem/CosColim-Adjunction.agda`.