2-coherence of Suspension-Loop adjunction

Dockerfile

@@ -29,7 +29,7 @@ RUN \
 
 FROM alpine AS hottagda
 
-COPY ["HoTT-Agda", "/build/Hott-Agda"]
+COPY ["HoTT-Agda", "/build/HoTT-Agda"]
 COPY ["Colimit-code", "/build/Colimit-code"]
 
 FROM alpine
@@ -40,10 +40,14 @@ COPY --from=hottagda /build /build
 COPY ["Pullback-stability", "/build/Pullback-stability"]
 COPY agda-html.sh /
 
-RUN echo "/build/Hott-Agda/hott-core.agda-lib" >> /dist/libraries
+RUN echo "/build/HoTT-Agda/hott-core.agda-lib" >> /dist/libraries
+RUN echo "/build/HoTT-Agda/hott-theorems.agda-lib" >> /dist/libraries
 RUN echo "/build/Colimit-code/cos-colim.agda-lib" >> /dist/libraries
 RUN echo "/build/Pullback-stability/stab.agda-lib" >> /dist/libraries
 
+WORKDIR /build/HoTT-Agda
+RUN /dist/agda --library-file=/dist/libraries ./theorems/homotopy/SuspAdjointLoop.agda
+
 WORKDIR /build/Colimit-code
 RUN /dist/agda --library-file=/dist/libraries ./R-L-R/CC-Equiv-RLR-0.agda
 RUN /dist/agda --library-file=/dist/libraries ./R-L-R/CC-Equiv-RLR-1.agda

HoTT-Agda/README.md

@@ -2,8 +2,10 @@ Homotopy Type Theory in Agda
 ============================
 
 This directory contains a heavily stripped-down version of Andrew Swan's [branch](https://github.com/awswan/HoTT-Agda/tree/agda-2.6.1-compatible) of the
-HoTT-Agda library. It also contains a bunch of additional lemmas, which arose during our
-development of coslice colimits. The structure of the source code is described below.
+HoTT-Agda library. It also contains a bunch of additional auxiliary lemmas, which arose
+during our development of coslice colimits. Finally, it contains a new verification of the
+2-coherence of the Suspension-Loop adjunction, which itself relies on a bunch of new auxiliary
+lemmas. The structure of the source code is described below.
 
 Setup
 -----
@@ -28,9 +30,17 @@ The main library is more or less divided into two parts.
 - The first part is exported in the module `lib.Basics` and contains everything needed to make the second
   part compile.
 - The second part is found in `lib.types` and develops type formers.
+  Note that it contains new facts about homogeneous types and reformulates some of the basic theory of
+  the Suspension type.
 
 Note that our work on colimits makes extensive use of the `path-seq/` directory.
 
+### Homotopy (directory `theorems/homotopy/`)
+
+This directory contains a proof of the 2-coherence of the Suspension-Loop adjunction.
+This property of the adjunction is important because it ensures that the Suspension
+functor preserves colimits. The proof relies on our work on homogeneous types.
+
 Citation
 --------
 

HoTT-Agda/core/lib/Function.agda

@@ -23,35 +23,11 @@ _∼_ : ∀ {i j} {A : Type i} {B : A → Type j}
   (f g : (a : A) → B a) → Type (lmax i j)
 f ∼ g = ∀ x → f x == g x
 
-{-
-infixr 80 _∼-∙_
-
-_∼-∙_ : ∀ {i j} {A : Type i} {B : Type j} {f g h : A → B}
-  → f ∼ g → g ∼ h → f ∼ h
-_∼-∙_ f∼g g∼h x = f∼g x ∙ g∼h x
-
-∼-! : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
-  → f ∼ g → g ∼ f
-∼-! f∼g = ! ∘ f∼g
--}
-
 _⊙∼_ : ∀ {i j} {X : Ptd i} {Y : Ptd j}
   (f g : X ⊙→ Y) → Type (lmax i j)
 _⊙∼_ {X = X} {Y = Y} (f , f-pt) (g , g-pt) =
   Σ (f ∼ g) λ p → f-pt == g-pt [ (_== pt Y) ↓ p (pt X) ]
 
-{-
-infixr 80 _⊙∼-∙_
-
-_⊙∼-∙_ : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g h : X ⊙→ Y}
-  → f ⊙∼ g → g ⊙∼ h → f ⊙∼ h
-_⊙∼-∙_ f∼g g∼h = fst f∼g ∼-∙ fst g∼h , snd f∼g ∙ᵈ snd g∼h
-
-⊙∼-! : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
-  → f ⊙∼ g → g ⊙∼ f
-⊙∼-! f∼g = ∼-! (fst f∼g) , !ᵈ (snd f∼g)
--}
-
 infixr 80 _⊙∘_
 _⊙∘_ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
   (g : Y ⊙→ Z) (f : X ⊙→ Y) → X ⊙→ Z

HoTT-Agda/core/lib/PathFunctor.agda

@@ -16,6 +16,10 @@ module _ {i j} {A : Type i} {B : Type j} (f : A → B) where
     → ap f (! p) == ! (ap f p)
   ap-! idp = idp
 
+  ap-!-inv : {x y : A} (p : x == y)
+    → ap f p ∙ ap f (! p) == idp
+  ap-!-inv idp = idp
+
   ∙-ap : {x y z : A} (p : x == y) (q : y == z)
     → ap f p ∙ ap f q == ap f (p ∙ q)
   ∙-ap idp q = idp
@@ -36,6 +40,10 @@ module _ {i j} {A : Type i} {B : Type j} (f : A → B) where
     → ap f (p ∙ q ∙ r) == ap f p ∙ ap f q ∙ ap f r
   ap-∙∙ idp idp r = idp
 
+  ap-!∙∙ : {x y z w : A} (p : y == x) (q : y == z) (r : z == w)
+    → ap f (! p ∙ q ∙ r) == ! (ap f p) ∙ ap f q ∙ ap f r
+  ap-!∙∙ idp idp r = idp
+
   ap-∙∙∙ : {x y z w t : A} (p : x == y) (q : y == z) (r : z == w) (s : w == t)
     → ap f (p ∙ q ∙ r ∙ s) == ap f p ∙ ap f q ∙ ap f r ∙ ap f s
   ap-∙∙∙ idp idp idp s = idp
@@ -46,6 +54,15 @@ module _ {i j} {A : Type i} {B : Type j} (f : A → B) where
 
   -- note: ap-∙' is defined in PathGroupoid
 
+  module _ {k} {C : Type k} (g : B → C) where
+
+    ap3-!-ap-!-rid : {x y : A} (p₁ : x == y)
+      {e : f x == f y} (p₂ : ap f p₁ == e) →
+      ap (ap g) (ap (λ p → p) (! (ap-! p₁ ∙ ap ! (p₂ ∙ idp))))
+      ==
+      ap (λ p → ap g (! p)) (! p₂) ∙ ap (ap g) (!-ap p₁)
+    ap3-!-ap-!-rid idp idp = idp
+
 {- Dependent stuff -}
 module _ {i j} {A : Type i} {B : A → Type j} (f : Π A B) where
 
@@ -79,10 +96,41 @@ module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
 
 module _ {i j} {A : Type i} {B : Type j} (g : A → B) where
 
+  !-ap-∙ : {x y : A} (p : x == y) {z : A} (r : x == z) → ! (ap g p) ∙ ap g r == ap g (! p ∙ r)
+  !-ap-∙ idp r = idp
+
+  ap-!-∙-ap : ∀ {k} {C : Type k} (h : C → A) {y z : C} {x : A} (q : y == z) (p : x == h y) 
+    →  ap g (! p) ∙ ap g (p ∙ ap h q) == ap g (ap h q)
+  ap-!-∙-ap h q idp = idp 
+
   !-ap-∙-s : {x y : A} (p : x == y) {z : A} {r : x == z} {w : B} {s : g z == w}
     → ! (ap g p) ∙ ap g r ∙ s == ap g (! p ∙ r) ∙ s
   !-ap-∙-s idp = idp
 
+  !-∙-ap-∙'-! : {x w : B} {y z : A} (p : x == g y) (q : y == z) (r : w == g z)
+    → ! (p ∙ ap g q ∙' ! r) == r ∙ ap g (! q) ∙' ! p
+  !-∙-ap-∙'-! idp q idp = !-ap g q
+
+  !-∙-ap-∙'-!-coher : {y : A} {x : B} (p : x == g y) →
+    ! (!-inv-r p) ∙ ap (_∙_ p) (! (∙'-unit-l (! p)))
+    ==
+    ap ! (! (!-inv-r p) ∙ ap (_∙_ p) (! (∙'-unit-l (! p)))) ∙
+    !-∙-ap-∙'-! p idp p
+  !-∙-ap-∙'-!-coher idp = idp
+
+  idp-ap-!-!-∙-∙' : {x y : A} (p : x == y)
+    → idp == ap g (! p) ∙ ap g (p ∙ idp ∙' ! p) ∙' ! (ap g (! p))
+  idp-ap-!-!-∙-∙' idp = idp  
+
+  idp-ap-!-!-∙-∙'-coher : {x y : A} (p : x == y) →
+    ! (!-inv-r (ap g (! p))) ∙
+    ap (_∙_ (ap g (! p))) (! (∙'-unit-l (! (ap g (! p)))))
+    ==
+    idp-ap-!-!-∙-∙' p ∙
+    ! (ap (λ q → ap g (! p) ∙ ap g q ∙' ! (ap g (! p)))
+      (! (!-inv-r p) ∙ ap (_∙_ p) (! (∙'-unit-l (! p))))) ∙ idp
+  idp-ap-!-!-∙-∙'-coher idp = idp
+
 module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B) where
 
   ∘-ap : {x y : A} (p : x == y) → ap g (ap f p) == ap (g ∘ f) p
@@ -91,9 +139,31 @@ module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A →
   ap-∘ : {x y : A} (p : x == y) → ap (g ∘ f) p == ap g (ap f p)
   ap-∘ idp = idp
 
+  ap-∘-∘ : ∀ {l} {D : Type l} (h : D → A) {x y : D} (p : x == y)
+    → ap (g ∘ f ∘ h) p == ap g (ap f (ap h p))
+  ap-∘-∘ h idp = idp
+
   !ap-∘=∘-ap : {x y : A} (p : x == y) → ! (ap-∘ p) == ∘-ap p
   !ap-∘=∘-ap idp = idp
 
+  ap-∘2-ap-! : {x y : A} (v : x == y)
+    {c : g (f (y)) == g (f x)} (e : ap g (! (ap f v)) == c) 
+    → (! (ap (λ q → q) (ap-∘ (! v) ∙
+      ap (ap g) (ap-! f v))) ∙ idp) ∙
+      ap-∘ (! v) ∙
+      ap (ap g) (ap (λ p → p) (ap-! f v)) ∙ e
+      == e
+  ap-∘2-ap-! idp e = idp 
+
+  ap-∘2-ap-∙ : {x y : A} (v : x == y) → 
+    ! (ap (ap g) (ap-∙ f v idp ∙ idp)) ∙
+    ! (ap (λ q → q) (ap-∘ (v ∙ idp))) ∙
+    ! (! (ap (λ p → p ∙ idp) (ap-∘ v)) ∙
+      ! (ap-∙ (g ∘ f) v idp))
+    ==
+    ap-∙ g (ap f v) idp ∙ idp
+  ap-∘2-ap-∙ idp = idp
+
   ap-cp-rev : {w : C} {z : B} {x y : A} (p : x == y) (q : f x == z) (r : g (f y) == w) →
     ! (ap g q) ∙ ap (g ∘ f) p ∙ r == ! (ap g (! (ap f p) ∙ q)) ∙  r
   ap-cp-rev idp q r = idp
@@ -110,6 +180,18 @@ module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A →
     → ! (ap (g ∘ f) p) ∙ (ap g S ∙ gₚ) ∙ ! (ap g (! (ap f p) ∙ S ∙ idp) ∙ gₚ) == idp
   inv-canc-cmp idp idp idp = idp
 
+  ap-!-∘-rid-coher : {x y : A} (p : x == y)
+    → ! (ap (λ q →  (ap g (ap f p)) ∙ q) (ap-∘ (! p) ∙ ap (ap g) (ap-! f p))) ∙ idp
+      ==
+      ap-!-inv g (ap f p) ∙ ! (cmp-inv-r p)
+  ap-!-∘-rid-coher idp = idp
+
+  ap-!-∘-∙-rid-coher : {x y : A} (p : x == y)
+    → ! (! (cmp-inv-r p) ∙ ! (ap (λ q → q ∙ ap (g ∘ f) (! p)) (ap-∘ p)) ∙ ! (ap-∙ (g ∘ f) p (! p))) ∙ idp
+      ==
+      ap (ap (g ∘ f)) (!-inv-r p) ∙ idp
+  ap-!-∘-∙-rid-coher idp = idp
+
 {- ap of idf -}
 ap-idf : ∀ {i} {A : Type i} {u v : A} (p : u == v) → ap (idf A) p == p
 ap-idf idp = idp
@@ -292,6 +374,12 @@ module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A →
     → ap-∘-∙-coh-seq₁ p p' =ₛ ap-∘-∙-coh-seq₂ p p'
   ap-∘-∙-coh idp idp = =ₛ-in idp
 
+  ap-∘-long : (h : A → B) (K : (z : A) → h z == f z) {x y : A} (p : x == y) →
+    ap (g ∘ f) p
+    ==
+    ap g (! (K x)) ∙ ap g (K x ∙ ap f p ∙' ! (K y)) ∙' ! (ap g (! (K y)))
+  ap-∘-long h K {x} idp = idp-ap-!-!-∙-∙' g (K x)
+
 module _ {i j} {A : Type i} {B : Type j} (b : B) where
 
   ap-cst : {x y : A} (p : x == y)
@@ -389,6 +477,17 @@ module _ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f g : A → B} (H
   hmtpy-nat-! : {x y : A} (p : x == y) → ! (H x) == ap g p ∙ ! (H y) ∙ ! (ap f p)
   hmtpy-nat-! {x = x} idp = ! (∙-unit-r (! (H x)))
 
+  hmtpy-nat-!-sq : {x y : A} (p : x == y) → ! (H x) ∙ ap f p == ap g p ∙ ! (H y)
+  hmtpy-nat-!-sq {x = x} idp = ∙-unit-r (! (H x))
+
+  hmpty-nat-∙'-r : {x y : A} (p : x == y) →  ap f p ==  H x ∙ ap g p ∙' ! (H y)
+  hmpty-nat-∙'-r {x} idp = ! (!-inv-r (H x)) ∙ ap (λ p → H x ∙ p) (! (∙'-unit-l (! (H x))))
+
+module _ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B} where
+
+  hmpty-nat-∙'-r-idp : {x y : A} (p : x == y) → hmpty-nat-∙'-r {f = f} (λ x → idp) p == idp
+  hmpty-nat-∙'-r-idp idp = idp
+
 module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} {D : Type ℓ₄} {f : A → B} {g : A → C}
   (v : B → D) (u : C → D) (H : (x : A) → v (f x) == u (g x)) where
 
@@ -469,11 +568,14 @@ module _ {i j k} {A : Type i} {B : Type j} {C : Type k} where
 
 module _ {i} {A : Type i} where
 
-  -- unsure where this belongs
   transp-cst=idf : {a x y : A} (p : x == y) (q : a == x)
     → transport (λ x → a == x) p q == q ∙ p
   transp-cst=idf idp q = ! (∙-unit-r q)
 
+  transp-cst=idf-l : {a x y : A} (p : x == y) (q : x == a)
+    → transport (λ x → x == a) p q == ! p ∙ q
+  transp-cst=idf-l idp q = idp
+
   transp-cst=idf-pentagon : {a x y z : A}
     (p : x == y) (q : y == z) (r : a == x)
     → transp-cst=idf (p ∙ q) r ◃∎ =ₛ

HoTT-Agda/core/lib/PathGroupoid.agda

@@ -47,6 +47,10 @@ module _ {i} {A : Type i} where
     → (p ∙' q) ∙ r == p ∙ (q ∙ r)
   ∙'∙-∙∙-assoc p idp r = idp
 
+  assoc-4-∙ : {x₁ x₂ x₃ x₄ x₅ x₆ : A} (p₁ : x₁ == x₂) (p₂ : x₂ == x₃) (p₃ : x₃ == x₄) (p₄ : x₄ == x₅) (p₅ : x₅ == x₆)
+    → p₁ ∙ p₂ ∙ p₃ ∙ p₄ ∙ p₅ == (p₁ ∙ p₂ ∙ p₃) ∙ p₄ ∙ p₅
+  assoc-4-∙ idp idp p₃ p₄ p₅ = idp 
+
   -- [∙-unit-l] and [∙'-unit-r] are definitional
 
   ∙-unit-r : {x y : A} (q : x == y) → q ∙ idp == q
@@ -93,9 +97,61 @@ module _ {i} {A : Type i} where
   !-! : {x y : A} (p : x == y) → ! (! p) == p
   !-! idp = idp
 
+  ∙-idp-!-∙'-rot : {x y : A} (p : x == y) (q : x == y)
+    → idp == p ∙ idp ∙' ! q → p == q
+  ∙-idp-!-∙'-rot idp q e = ap ! (e ∙ ∙'-unit-l (! q)) ∙ !-! q
+
+{- additional algebraic lemmas -}
+
+module _ {i} {A : Type i} where
+
+  ∙-∙'-!-rot : {x y z w : A} (p₀ : x == y) (p₁ : x == z) (p₂ : z == w) (p₃ : y == w)
+    → p₀ == p₁ ∙ p₂  ∙' ! p₃ → p₂ == ! p₁ ∙ p₀ ∙' p₃
+  ∙-∙'-!-rot p₀ idp p₂ idp e = ! e
+
+  !-inj-rot : {x y : A} {p₁ p₂ : x == y} (n : p₁ == p₂) {m : ! p₁ == ! p₂}
+    → m == ap ! n →  ! (!-! p₁) ∙ ap ! m ∙' !-! p₂ == n
+  !-inj-rot {p₁ = idp} idp idp = idp
+
+  ∙'-!-∙-∙ : {x y z w : A} (p₁ : x == y) (p₂ : z == y) (p₃ : y == w)
+    → (p₁ ∙' ! p₂) ∙ p₂ ∙ p₃ == p₁ ∙ p₃
+  ∙'-!-∙-∙ p₁ idp p₃ = idp
+
+  !-inv-l-r-unit-assoc : {x y : A} (p : x == y) →
+    ! (ap (λ c → p ∙ c) (!-inv-l p) ∙ ∙-unit-r p) ∙
+    ! (∙-assoc p (! p) p) ∙ ap (λ c → c ∙ p) (!-inv-r p)
+    == idp
+  !-inv-l-r-unit-assoc idp = idp
+
+  assoc-tri-!-mid : {x y z w u v : A} (p₀ : x == y) (p₁ : y == z) (p₂ : w == z)
+    (p₃ : z == u) (p₄ : u == v)
+    → (p₀ ∙ p₁ ∙' ! p₂) ∙ p₂ ∙ p₃ ∙' p₄ == p₀ ∙ (p₁ ∙ p₃) ∙' p₄
+  assoc-tri-!-mid idp p₁ p₂ p₃ idp = ∙'-!-∙-∙ p₁ p₂ p₃
+
+  assoc-tri-!-coher : {x y : A} (p : x == y) →
+    ! (!-inv-r p) ∙ ap (_∙_ p) (! (∙'-unit-l (! p))) ==
+    ap (λ q → q ∙ idp)
+      (! (!-inv-r p) ∙ ap (_∙_ p) (! (∙'-unit-l (! p)))) ∙
+    ap (_∙_ (p ∙ idp ∙' ! p))
+      (! (!-inv-r p) ∙ ap (_∙_ p) (! (∙'-unit-l (! p)))) ∙
+    assoc-tri-!-mid p idp p idp (! p) ∙ idp
+  assoc-tri-!-coher idp = idp
+
   inv-rid : {x y : A} (p : x == y) → ! p ∙ p ∙ idp == idp
   inv-rid idp = idp
 
+  !3-∙3 : {x y z w : A} (p : x == y) (q : z == y) (r : w == y)
+    → ! ((p ∙ ! q) ∙ q ∙ ! r) ∙ p == r
+  !3-∙3 idp idp r = ∙-unit-r (! (! r)) ∙ !-! r
+
+  ∙-∙'-= : {x y : A} {p r : x == y} (q : x == x)
+    → p == r → ! p ∙ q ∙' p == ! r ∙ q ∙' r
+  ∙-∙'-= q idp = idp
+
+  tri-exch : {x y z : A} {p : y == x} {q : y == z} {r : x == z}
+    → ! p ∙ q == r → p == q ∙ ! r
+  tri-exch {p = idp} {q = idp} {r} e = ap ! e
+
   {- Horizontal compositions -}
 
   infixr 80 _∙2_ _∙'2_
@@ -123,6 +179,9 @@ module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type 
   cmp-inv-l : {x y : A} (p : x == y) → ! (ap (g ∘ f) p) ∙ ap g (ap f p) == idp
   cmp-inv-l idp = idp
 
+  cmp-inv-r : {x y : A} (p : x == y) → ap g (ap f p) ∙ (ap (g ∘ f) (! p)) == idp
+  cmp-inv-r idp = idp
+
   cmp-inv-rid : {x y : A} (p : x == y) → idp == ap (g ∘ f) p ∙ ! (ap g (ap f p) ∙ idp)
   cmp-inv-rid idp = idp