Simpler proof of naturality square

.dockerignore

@@ -1,2 +1,3 @@
 _build
-README.md
+*.md
+*.txt

.github/workflows/agda.yml

@@ -3,7 +3,13 @@ on:
   push:
     branches:
       - main
+    paths-ignore:
+      - '**.md'
+      - '**.txt'
   pull_request:
+    paths-ignore:
+      - '**.md'
+      - '**.txt'
 jobs:
   build:
     runs-on: ubuntu-latest

Colimit-code/Aux/AuxPaths-v2.agda

@@ -2,15 +2,9 @@
 
 open import lib.Basics
 open import FTID
-open import AuxPaths
 
 module AuxPaths-v2 where
 
-module _  {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l} {f : A → B}  {h : C → A} {v : C → D} {u : D → B} where
-
-  pth-tri-∘ : (q : u ∘ v ∼ f ∘ h) {x y : C} (p : x == y) →  ! (ap u (ap v p)) ∙ q x ∙ ap f (ap h p) == q y
-  pth-tri-∘ q {x = x} idp = ∙-unit-r (q x)
-
 module _ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B} {x : A} {z : B} where
 
   E₁-v2 : ∀ {ℓ₃} {C : Type ℓ₃} {g : C → A} {c d : C} {R : g c == x} {S : f (g d) == z} (Q : c == d)

Colimit-code/Aux/AuxPaths.agda

@@ -16,6 +16,12 @@ module _ {ℓ₁ ℓ₂ k l} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B} {
     → ! (ap u S) ∙ q x ∙ L x ∙ ap f (ap h p) == q y ∙ L y
   E₃ q {x = x} idp idp L = ap (λ p → q x ∙ p) (∙-unit-r (L x)) 
 
+module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} (h : A → C) (g : C → B) where
+
+  !-!-ap-∘ : {x y : A} (p : x == y) {b : B} (q : b == g (h y))
+    → ! (q ∙ ap g (! (ap h p))) == ap (g ∘ h) p ∙ ! q
+  !-!-ap-∘ idp q = ap ! (∙-unit-r q)
+
 module _ {i j} {A : Type i} {B : Type j} {f g h : A →  B} {F : (x : A) → f x == g x} {G : (x : A) → g x == h x} where
 
   apd-∙-r : {x y : A} (κ : x == y) → transport (λ z → f z == h z) κ (F x ∙ G x) == transport (λ z → f z == g z) κ (F x) ∙ G y
@@ -31,3 +37,6 @@ module _ {i j k} {A : Type i} {B : Type j} {C : Type k} {g h : A → B} {f : A 
 
   apd-ap-∙-l-coher : {x y : A} (κ : x == y) → apd-tr (λ z → F z ∙ ap ψ (! (G z))) κ ◃∎  =ₛ apd-ap-∙-l κ ◃∙ ap (λ p → F y ∙ ap ψ (! p)) (apd-tr G κ) ◃∎
   apd-ap-∙-l-coher idp = =ₛ-in idp
+
+  apd-ap-∙-l-! : {x y : A} (κ : x == y) → transport (λ z →  ψ (h z) == f z) κ (! (F x ∙ ap ψ (! (G x)))) == ! (F y ∙ ap ψ (! (transport (λ z → h z == g z) κ (G x))))
+  apd-ap-∙-l-! idp = idp

Colimit-code/Aux/Cocone-switch.agda

@@ -1,10 +1,8 @@
 {-# OPTIONS --without-K --rewriting  #-}
 
 open import lib.Basics
-open import lib.types.Sigma
 open import lib.types.Pushout
 open import lib.types.Span
-open import lib.PathSeq
 open import Coslice
 open import Diagram
 open import Colim

Colimit-code/Aux/Cocone-v2.agda

@@ -8,7 +8,6 @@
 open import lib.Basics
 open import lib.types.Pushout
 open import lib.types.Span
-open import lib.PathSeq
 open import Coslice
 open import Diagram
 open import Colim
@@ -37,18 +36,22 @@ module CC-v2-Constr {ℓv ℓe ℓ ℓd} {Γ : Graph ℓv ℓe} {A : Type ℓ} (
     →  E₁ {f = right} {g = cin j} idp q == E₂-v2 {f = right} {p = ap ψ (cglue g a)} idp q
   E-eq-helper idp = idp
 
-  E-eq : (q : (z : Colim (ConsDiag Γ A)) →  right {d = SpCos} (ψ z) == left ([id] z)) {x : ty (F # j)} (σ : x == fun (F # j) a) (T₁ : ap [id] (cglue g a) == idp)
-    (R : cin j x == ψ (cin i a)) (T₂ : ap ψ (cglue g a) == ! (ap (cin j) σ) ∙ R)
-    → E₁ σ (q (cin j a)) ◃∙ ! (ap (λ p → ! (ap right (! (ap (cin j) σ) ∙ R)) ∙ q (cin j a) ∙ p) (ap (ap left) T₁)) ◃∙ E₃ q (cglue g a) T₂ (λ z → idp) ◃∙ ∙-unit-r (q (cin i a)) ◃∎
+  E-eq : (q : (z : Colim (ConsDiag Γ A)) →  right {d = SpCos} (ψ z) == left ([id] z)) {x : ty (F # j)} (σ : x == fun (F # j) a)
+    (T₁ : ap [id] (cglue g a) == idp) (R : cin j x == ψ (cin i a)) (T₂ : ap ψ (cglue g a) == ! (ap (cin j) σ) ∙ R)
+    → E₁ σ (q (cin j a)) ◃∙ ! (ap (λ p → ! (ap right (! (ap (cin j) σ) ∙ R)) ∙ q (cin j a) ∙ p) (ap (ap left) T₁)) ◃∙
+      E₃ q (cglue g a) T₂ (λ z → idp) ◃∙
+      ∙-unit-r (q (cin i a)) ◃∎
       =ₛ
     E₁-v2 σ ◃∙ E₂-v2 T₂ (q (cin j a)) ◃∙ E₃-v2 {f = left} q (cglue g a) T₁ ◃∎
   E-eq q idp T₁ R T₂ = =ₛ-in (lemma R T₂)
     where
       lemma : (r : ψ (cin j a) == ψ (cin i a)) (τ : ap ψ (cglue g a) == r)
-        → E₁ {f = right} {g = cin j} idp (q (cin j a)) ∙ ! (ap (λ p → ! (ap right r) ∙ q (cin j a) ∙ p) (ap (ap left) T₁)) ∙ E₃ q (cglue g a) τ (λ z → idp) ∙ ∙-unit-r (q (cin i a))
+        → E₁ {f = right} {g = cin j} idp (q (cin j a)) ∙ ! (ap (λ p → ! (ap right r) ∙ q (cin j a) ∙ p) (ap (ap left) T₁)) ∙
+          E₃ q (cglue g a) τ (λ z → idp) ∙ ∙-unit-r (q (cin i a))
         == E₂-v2 τ (q (cin j a)) ∙ E₃-v2 {f = left} {u = right} q (cglue g a) T₁
-      lemma r idp = ap (λ p → p ∙ ! (ap (λ p → ! (ap right (ap ψ (cglue g a))) ∙ q (cin j a) ∙ p) (ap (ap left) T₁)) ∙ E₃ q (cglue g a) idp (λ z → idp) ∙ ∙-unit-r (q (cin i a)))
-        (E-eq-helper (q (cin j a))) ∙ ap (λ p → E₂-v2 {f = right} {p = ap ψ (cglue g a)} idp (q (cin j a)) ∙ p) (lemma2 (cglue g a) T₁)
+      lemma r idp = ap (λ p → p ∙ ! (ap (λ p → ! (ap right (ap ψ (cglue g a))) ∙ q (cin j a) ∙ p) (ap (ap left) T₁)) ∙
+        E₃ q (cglue g a) idp (λ z → idp) ∙ ∙-unit-r (q (cin i a))) (E-eq-helper (q (cin j a))) ∙
+        ap (λ p → E₂-v2 {f = right} {p = ap ψ (cglue g a)} idp (q (cin j a)) ∙ p) (lemma2 (cglue g a) T₁)
           where
             lemma2 : {y : Colim (ConsDiag Γ A)} (c : (cin j a) == y) {v : a == [id] y} (t : ap [id] c == v)
               → ! (ap (λ p → ! (ap right (ap ψ c)) ∙ q (cin j a) ∙ p) (ap (ap left) t)) ∙ E₃ q c idp (λ z → idp) ∙ ∙-unit-r (q y) == E₃-v2 q c t

Colimit-code/Aux/Cocone.agda

@@ -3,10 +3,8 @@
 {- Formation of A-cocone structure on pushout -}
 
 open import lib.Basics
-open import lib.types.Sigma
 open import lib.types.Pushout
 open import lib.types.Span
-open import lib.PathSeq
 open import Coslice
 open import Diagram
 open import Colim
@@ -16,12 +14,14 @@ module Cocone where
 
 module _ {ℓ₁ ℓ₂} {B : Type ℓ₁} {D : Type ℓ₂} {u : D → B} where
 
-  H₁ : ∀ {k l} {C : Type k} {A : Type l} {h : C → A} {f : A → B} {v : C → D} {c d : C} (Q : c == d) (s : f (h c) == u (v c)) {q : v c == v d} (R : ap v Q == q)
-    → transport (λ x → f (h x) == u (v x)) Q s == ! (ap f (ap h Q)) ∙ s ∙ ap u q
+  H₁ : ∀ {k l} {C : Type k} {A : Type l} {h : C → A} {f : A → B} {v : C → D} {c d : C} (Q : c == d) (s : f (h c) == u (v c))
+    {q : v c == v d} (R : ap v Q == q) →
+    transport (λ x → f (h x) == u (v x)) Q s == ! (ap f (ap h Q)) ∙ s ∙ ap u q
   H₁ idp s idp = ! (∙-unit-r s)
 
-  H₂ : ∀ {ℓ₃} {E : Type ℓ₃} {x y : B} {g : E → D} {d e : E} (t : d == e) (q : u (g e) == y) {p : x == y} {z : D} (s : g d == z) {R : u (g d) == u z} (T : ap u s == R)
-    → p ∙ ! q ∙ ap u (! (ap g t) ∙ s) == p ∙ ! (! R ∙ ap (u ∘ g) t ∙ q)
+  H₂ : ∀ {ℓ₃} {E : Type ℓ₃} {x y : B} {g : E → D} {d e : E} (t : d == e) (q : u (g e) == y) {p : x == y} {z : D} (s : g d == z)
+    {R : u (g d) == u z} (T : ap u s == R) →
+    p ∙ ! q ∙ ap u (! (ap g t) ∙ s) == p ∙ ! (! R ∙ ap (u ∘ g) t ∙ q)
   H₂ idp q {p = p} idp idp = ap (λ r → p ∙ r) (∙-unit-r (! q))
 
 module Id {ℓv ℓe ℓ} (Γ : Graph ℓv ℓe) (A : Type ℓ) where
@@ -58,15 +58,17 @@ module Id {ℓv ℓe ℓ} (Γ : Graph ℓv ℓe) (A : Type ℓ) where
       module _ where
       ϵ : ∀ {i j} (g : Hom Γ i j) (a : A) →
         ! (ap right (cglue g (fun (F # i) a))) ∙ ap (right ∘ cin j) (snd (F <#> g) a) ∙ ! (glue (cin j a)) =-= ! (glue (cin i a))
-      ϵ {i} {j} g a = ! (ap right  (cglue g (fun (F # i) a))) ∙ (ap (right ∘ cin j) (snd (F <#> g) a)) ∙ (! (glue (cin j a)))
-                        =⟪ E₁ (snd (F <#> g) a) (! (glue (cin j a))) ⟫
-                      ! (ap right (! (ap (cin j) (snd (F <#> g) a)) ∙ cglue g (fun (F # i) a))) ∙ ! (glue (cin j a)) ∙ idp
-                        =⟪ ! (ap (λ p → ! (ap right (! (ap (cin j) (snd (F <#> g) a)) ∙ cglue g (fun (F # i) a))) ∙ ! (glue (cin j a)) ∙ p) (ap (ap left) (id-βr g a)))  ⟫
-                      ! (ap right (! (ap (cin j) (snd (F <#> g) a)) ∙ cglue g (fun (F # i) a))) ∙ ! (glue (cin j a)) ∙ ap left (ap [id] (cglue g a))
-                        =⟪ E₃ (λ x → ! (glue x)) (cglue g a) (ψ-βr g a) (λ x → idp) ⟫
-                      ! (glue (cin i a)) ∙ idp
-                        =⟪ ∙-unit-r (! (glue (cin i a)))  ⟫
-                      ! (glue (cin i a)) ∎∎
+      ϵ {i} {j} g a =
+        ! (ap right  (cglue g (fun (F # i) a))) ∙ (ap (right ∘ cin j) (snd (F <#> g) a)) ∙ (! (glue (cin j a)))
+          =⟪ E₁ (snd (F <#> g) a) (! (glue (cin j a))) ⟫
+        ! (ap right (! (ap (cin j) (snd (F <#> g) a)) ∙ cglue g (fun (F # i) a))) ∙ ! (glue (cin j a)) ∙ idp
+          =⟪ ! (ap (λ p → ! (ap right (! (ap (cin j) (snd (F <#> g) a)) ∙ cglue g (fun (F # i) a))) ∙ ! (glue (cin j a)) ∙ p)
+            (ap (ap left) (id-βr g a))) ⟫
+        ! (ap right (! (ap (cin j) (snd (F <#> g) a)) ∙ cglue g (fun (F # i) a))) ∙ ! (glue (cin j a)) ∙ ap left (ap [id] (cglue g a))
+          =⟪ E₃ (λ x → ! (glue x)) (cglue g a) (ψ-βr g a) (λ x → idp) ⟫
+        ! (glue (cin i a)) ∙ idp
+          =⟪ ∙-unit-r (! (glue (cin i a))) ⟫
+        ! (glue (cin i a)) ∎∎
 
     module Recc {ℓc} (T : Coslice ℓc ℓ A) where
 
@@ -86,18 +88,19 @@ module Id {ℓv ℓe ℓ} (Γ : Graph ℓv ℓe) (A : Type ℓ) where
           σ = colimE (λ i → (λ a → ! (snd (r i) a)))
             (λ i → (λ j → (λ g → (λ a →   from-transp-g (λ z → fun T ([id] z) == recc (ψ z)) (cglue g a) (↯ (η i j g a))))))
               module _ where
-                η : (i j : Obj Γ) (g : Hom Γ i j) (a : A) → transport (λ z → fun T ([id] z) ==  recc (ψ z)) (cglue g a) (! (snd (r j) a)) =-= ! (snd (r i) a)
+                η : (i j : Obj Γ) (g : Hom Γ i j) (a : A) →
+                  transport (λ z → fun T ([id] z) == recc (ψ z)) (cglue g a) (! (snd (r j) a)) =-= ! (snd (r i) a)
                 η i j g a =
-                            transport (λ z →  fun T ([id] z) == recc (ψ z)) (cglue g a) (! (snd (r j) a))
-                              =⟪ H₁ (cglue g a) (! (snd (r j) a)) (ψ-βr g a) ⟫
-                            ! (ap (fun T) (ap [id] (cglue g a))) ∙ (! (snd (r j) a)) ∙ ap recc (! (ap (cin j) (snd (F <#> g) a)) ∙ (cglue g (fun (F # i) a)))
-                              =⟪ H₂ (snd (F <#> g) a) (snd (r j) a) (cglue g (fun (F # i) a)) (recc-βr (r & K) g (fun (F # i) a)) ⟫
-                            ! (ap (fun T) (ap [id] (cglue g a))) ∙ ! (! (fst (K g) (fun (F # i) a)) ∙ ap (recc ∘ cin j) (snd (F <#> g) a) ∙ (snd (r j) a))
-                              =⟪ ap (λ p → p ∙ ! (! (fst (K g) (fun (F # i) a)) ∙ ap (recc ∘ cin j) (snd (F <#> g) a) ∙ (snd (r j) a)))
-                                (ap (λ p → ! (ap (fun T) p)) (id-βr g a)) ⟫
-                            ! (! (fst (K g) (fun (F # i) a)) ∙ ap (recc ∘ cin j) (snd (F <#> g) a) ∙ (snd (r j) a))
-                              =⟪ ap ! (snd (K g) a) ⟫
-                            ! (snd (r i) a) ∎∎
+                  transport (λ z →  fun T ([id] z) == recc (ψ z)) (cglue g a) (! (snd (r j) a))
+                    =⟪ H₁ (cglue g a) (! (snd (r j) a)) (ψ-βr g a) ⟫
+                  ! (ap (fun T) (ap [id] (cglue g a))) ∙ (! (snd (r j) a)) ∙ ap recc (! (ap (cin j) (snd (F <#> g) a)) ∙ (cglue g (fun (F # i) a)))
+                    =⟪ H₂ (snd (F <#> g) a) (snd (r j) a) (cglue g (fun (F # i) a)) (recc-βr (r & K) g (fun (F # i) a)) ⟫
+                  ! (ap (fun T) (ap [id] (cglue g a))) ∙ ! (! (fst (K g) (fun (F # i) a)) ∙ ap (recc ∘ cin j) (snd (F <#> g) a) ∙ (snd (r j) a))
+                    =⟪ ap (λ p → p ∙ ! (! (fst (K g) (fun (F # i) a)) ∙ ap (recc ∘ cin j) (snd (F <#> g) a) ∙ (snd (r j) a)))
+                      (ap (λ p → ! (ap (fun T) p)) (id-βr g a)) ⟫
+                  ! (! (fst (K g) (fun (F # i) a)) ∙ ap (recc ∘ cin j) (snd (F <#> g) a) ∙ (snd (r j) a))
+                    =⟪ ap ! (snd (K g) a) ⟫
+                  ! (snd (r i) a) ∎∎
       snd (recCosCoc x) a = idp
 
       FPrecc-βr = λ (C : CosCocone A F T) → PushoutRec.glue-β {d = SpCos} (fun T) (recc (comp C) (comTri C)) (σ (comp C) (comTri C))
@@ -110,5 +113,5 @@ module Id {ℓv ℓe ℓ} (Γ : Graph ℓv ℓe) (A : Type ℓ) where
           σ-β {i} {j} g a = apd-to-tr (λ x → fun T ([id] x) == recc (comp C) (comTri C) (ψ x)) (σ (comp C) (comTri C)) (cglue g a)
             (↯ (η (comp C) (comTri C) i j g a))
             (cglue-β (λ i → (λ a → ! (snd (comp C i) a)))
-            (λ i → (λ j → ( λ g → (λ a →   from-transp-g (λ z → fun T ([id] z) == recc (comp C) (comTri C) (ψ z))
+            (λ i → (λ j → ( λ g → (λ a →  from-transp-g (λ z → fun T ([id] z) == recc (comp C) (comTri C) (ψ z))
             (cglue g a) (↯ (η (comp C) (comTri C) i j g a)))))) g a)

Colimit-code/Aux/Coslice.agda

@@ -3,7 +3,6 @@
 {- Coslice categories of the universe -}
 
 open import lib.Basics
-open import lib.types.Sigma
 
 module Coslice where
 

Colimit-code/Aux/Diagram.agda

@@ -97,7 +97,7 @@ open CosCocone public
 
 -- Some operations on coslice cocones
 
-module  _ {ℓi ℓj k} {A : Type ℓj} {Γ : Graph ℓv ℓe} {F : CosDiag ℓi ℓj A Γ} {C : Coslice k ℓj A} where
+module _ {ℓi ℓj k} {A : Type ℓj} {Γ : Graph ℓv ℓe} {F : CosDiag ℓi ℓj A Γ} {C : Coslice k ℓj A} where
 
   ForgCoc : (CosCocone A F C) → Cocone (DiagForg A Γ F) (ty C)
   comp (ForgCoc (K & _)) i = fst (K i)
@@ -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))
-      ∙ ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri K g) 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))