diff --git a/Dockerfile b/Dockerfile
index cf5e1a6..21c6a4f 100644
--- a/Dockerfile
+++ b/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
diff --git a/HoTT-Agda/README.md b/HoTT-Agda/README.md
index 6d3c033..c9cc8fb 100644
--- a/HoTT-Agda/README.md
+++ b/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
 --------
 
diff --git a/HoTT-Agda/core/lib/Function.agda b/HoTT-Agda/core/lib/Function.agda
index b6919b0..0717cb2 100644
--- a/HoTT-Agda/core/lib/Function.agda
+++ b/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
diff --git a/HoTT-Agda/core/lib/PathFunctor.agda b/HoTT-Agda/core/lib/PathFunctor.agda
index 68af853..e380111 100644
--- a/HoTT-Agda/core/lib/PathFunctor.agda
+++ b/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 ◃∎ =ₛ
diff --git a/HoTT-Agda/core/lib/PathGroupoid.agda b/HoTT-Agda/core/lib/PathGroupoid.agda
index 29790fd..4f892bd 100644
--- a/HoTT-Agda/core/lib/PathGroupoid.agda
+++ b/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
 
diff --git a/HoTT-Agda/core/lib/PathOver.agda b/HoTT-Agda/core/lib/PathOver.agda
index b6c2f6e..a20e710 100644
--- a/HoTT-Agda/core/lib/PathOver.agda
+++ b/HoTT-Agda/core/lib/PathOver.agda
@@ -4,6 +4,7 @@ open import lib.Base
 open import lib.PathFunctor
 open import lib.PathGroupoid
 open import lib.Equivalence
+open import lib.Function
 
 {- Structural lemmas about paths over paths
 
@@ -285,7 +286,6 @@ module _ {i j} {A : Type i} where
   to-transp-equiv B p =
     equiv to-transp (from-transp B p) (to-transp-β B p) (to-transp-η)
 
-
   from-transp! : (B : A → Type j)
     {a a' : A} (p : a == a')
     {u : B a} {v : B a'}
@@ -327,9 +327,81 @@ module _ {i j} {A : Type i} where
   from-transp-g B idp h = h
 
   apd-to-tr : (B : A → Type j) (f : (a : A) → B a) {x y : A} (p : x == y)
-    (s : transport B p (f x) == f y) → apd f p == from-transp-g B p s → apd-tr f p == s
+    (s : transport B p (f x) == f y)
+    → apd f p == from-transp-g B p s → apd-tr f p == s
   apd-to-tr B f idp s h = h
 
+-- hmpty-nat conversion
+
+module _ {i j} {A : Type i} {B : Type j} (f g : A → B) where
+
+  from-hmpty-nat : {x y : A} (p : x == y) {e₁ : f x == g x} {e₂ : f y == g y} 
+    → ap f p == e₁ ∙ ap g p  ∙' ! e₂ → e₁ == e₂ [ (λ z → f z == g z) ↓ p ]
+  from-hmpty-nat idp {e₁} {e₂} p = ∙-idp-!-∙'-rot e₁ e₂ p
+
+  module _ (K : (z : A) → f z == g z) where
+
+    apd-to-hnat : {x y : A} (p : x == y)
+      (m : ap f p == K x ∙ ap g p  ∙' ! (K y))
+      → apd K p == from-hmpty-nat p m → hmpty-nat-∙'-r K p == m
+    apd-to-hnat {x} idp m q = lemma (K x) m q
+      where
+        lemma : {x₁ x₂ : B} (v : x₁ == x₂) (n : idp == v ∙ idp ∙' ! v)
+          (r : idp == ∙-idp-!-∙'-rot v v n)
+          → ! (!-inv-r v) ∙ ap (_∙_ v) (! (∙'-unit-l (! v))) == n
+        lemma idp n r = !-inj-rot n (r ∙ ∙-unit-r (ap ! (n ∙ idp)) ∙ ap (ap !) (∙-unit-r n))
+
+    apd-to-hnat-∙ : {x y z : A} (p₁ : x == y) (p₂ : y == z)
+      {m₁ : ap f p₁ == K x ∙ ap g p₁  ∙' ! (K y)} {m₂ : ap f p₂ == K y ∙ ap g p₂  ∙' ! (K z)}
+      (τ₁ : hmpty-nat-∙'-r K p₁ == m₁) (τ₂ : hmpty-nat-∙'-r K p₂ == m₂)
+      → hmpty-nat-∙'-r K (p₁ ∙ p₂)
+        ==
+        ↯ (ap-∙ f p₁ p₂ ◃∙
+        ap (λ p → p ∙ ap f p₂) m₁ ◃∙
+        ap (λ p → (K x ∙ ap g p₁ ∙' ! (K y)) ∙ p) m₂ ◃∙
+        assoc-tri-!-mid (K x) (ap g p₁) (K y) (ap g p₂) (! (K z)) ◃∙
+        ap (λ p → K x ∙ p ∙' ! (K z)) (! (ap-∙ g p₁ p₂)) ◃∎)
+    apd-to-hnat-∙ {x} idp idp idp idp = assoc-tri-!-coher (K x)
+
+    apd-to-hnat-! : {x y : A} (p : x == y)
+      {m : ap f p == K x ∙ ap g p  ∙' ! (K y)} (τ : hmpty-nat-∙'-r K p == m)
+      → hmpty-nat-∙'-r K (! p) == ap-! f p ∙ ap ! m ∙ !-∙-ap-∙'-! g (K x) p (K y)
+    apd-to-hnat-! {x} idp idp = !-∙-ap-∙'-!-coher g (K x)
+
+    apd-to-hnat-ap! : ∀ {l} {C : Type l} (h : B → C) {x y : A} (p : x == y)
+      {m : ap f p == K x ∙ ap g p  ∙' ! (K y)} (τ : hmpty-nat-∙'-r K p == m)
+      → hmpty-nat-∙'-r (λ z → ap h (! (K z))) p ==
+      ap-∘-long h g f K p ∙
+      ! (ap (λ q → ap h (! (K x)) ∙ ap h q ∙' ! (ap h (! (K y)))) m) ∙
+      ! (ap (λ q → ap h (! (K x)) ∙ q ∙' ! (ap h (! (K y)))) (ap-∘ h f p))
+    apd-to-hnat-ap! h {x} idp idp = idp-ap-!-!-∙-∙'-coher h (K x)
+
+{-
+  A coordinate definition of homotopy of pointed functions.
+  We also call such a homotopy "unfolded." 
+-}
+
+module _ {i j} {X : Ptd i} {Y : Ptd j} where 
+
+  infixr 30 _⊙-comp_
+  _⊙-comp_ : (f g : X ⊙→ Y) → Type (lmax i j)
+  _⊙-comp_ f g = Σ (fst f ∼ fst g) λ H → ! (H (pt X)) ∙ snd f =-= snd g
+
+  comp-⊙∼ : {f g : X ⊙→ Y} (H : f ⊙∼ g) → ! (fst H (pt X)) ∙ snd f =-= snd g
+  comp-⊙∼ {f = f} H = ! (transp-cst=idf-l (fst H (pt X)) (snd f)) ◃∙ to-transp (snd H) ◃∎
+
+  ⊙-to-comp : {f g : X ⊙→ Y} → f ⊙∼ g → f ⊙-comp g
+  ⊙-to-comp H = fst H , comp-⊙∼ H  
+
+  comp-to-⊙ : {f g : X ⊙→ Y} → f ⊙-comp g → f ⊙∼ g
+  fst (comp-to-⊙ H) = fst H
+  snd (comp-to-⊙ {f} H) =
+    from-transp (_== pt Y) (fst H (pt X)) (transp-cst=idf-l (fst H (pt X)) (snd f) ∙ ↯ (snd H))
+
+  ⊙id-to-comp : {f g : X ⊙→ Y} (p : f == g) → f ⊙-comp g
+  fst (⊙id-to-comp idp) = λ x → idp
+  snd (⊙id-to-comp idp) = idp ◃∎
+
 {- Various other lemmas -}
 
 module _ {i j} {A : Type i} {B : Type j} where
diff --git a/HoTT-Agda/core/lib/path-seq/Rotations.agda b/HoTT-Agda/core/lib/path-seq/Rotations.agda
index 8cba730..4cdf6cb 100644
--- a/HoTT-Agda/core/lib/path-seq/Rotations.agda
+++ b/HoTT-Agda/core/lib/path-seq/Rotations.agda
@@ -26,6 +26,13 @@ pre-rotate-in {q = q} {p = idp} {r = r} e =
     =ₛ⟨ =ₛ-in (! (↯-∙∙ (idp ◃∎) r)) ⟩
   idp ◃∙ r ∎ₛ
 
+pre-rotate-in-↯-assoc : {a₀ a₁ a₂ a₃ a₄ : A} {q : a₁ == a₀} {p : a₁ == a₂} {r : a₀ == a₃}
+  {s₁ : a₃ =-= a₄} {s₂ : a₂ =-= a₄}
+  → q ◃∙ (r ∙ ↯ s₁) ◃∎ =ₛ (p ∙ ↯ s₂) ◃∎
+  → ↯ (! p ◃∙ q ◃∙ r ◃∎) ◃∙ s₁ =ₛ s₂
+pre-rotate-in-↯-assoc {q = idp} {p = idp} {r = idp} {s₁} {s₂} e =
+  =ₛ-in (↯-∙∙ (idp ◃∎) s₁ ∙ =ₛ-out e)
+
 pre-rotate-out : {a a' a'' : A} {p : a == a'} {q : a' =-= a''} {r : a =-= a''}
   → q =ₛ ! p ◃∙ r
   → p ◃∙ q =ₛ r
@@ -87,6 +94,14 @@ post-rotate-in : {a a' a'' : A}
 post-rotate-in {p = p} {r = r} {q = q} e =
   !ₛ (post-rotate'-in (!ₛ e))
 
+post↯-rotate-in : {a a' a'' : A} {r : a'' =-= a} {p : a' =-= a} {q : a' == a''}
+  → q ◃∎ =ₛ ↯ p ◃∙ ! (↯ r) ◃∎
+  → q ◃∙ r =ₛ p
+post↯-rotate-in {r = r} {p = p} {q = idp} e =
+  =ₛ-in (↯-∙∙ (idp ◃∎) r ∙ ap (λ v → v ∙ ↯ r) (=ₛ-out e) ∙
+    ∙-assoc (↯ p) (! (↯ r)) (↯ r) ∙ ap (λ v → ↯ p ∙ v) (!-inv-l (↯ r)) ∙
+    ∙-unit-r (↯ p))
+
 post-rotate-out : {a a' a'' : A}
   → {p : a =-= a'} {q : a' == a''} {r : a =-= a''}
   → p =ₛ r ∙▹ ! q
diff --git a/HoTT-Agda/core/lib/types/Homogeneous.agda b/HoTT-Agda/core/lib/types/Homogeneous.agda
new file mode 100644
index 0000000..5a8e9dc
--- /dev/null
+++ b/HoTT-Agda/core/lib/types/Homogeneous.agda
@@ -0,0 +1,194 @@
+{-# OPTIONS --without-K --rewriting #-}
+
+open import lib.Basics
+open import lib.types.Pointed
+open import lib.types.LoopSpace
+open import lib.types.Paths
+open import lib.types.Sigma
+
+module lib.types.Homogeneous where
+
+-- homogeneous types satisfying a coherence condition at the basepoint
+
+module _ {i} {X : Type i} where
+
+  module _ (x : X) where
+
+    record homogeneous : Type i where
+      constructor homog
+      field
+        auto : (y : X) → ⊙[ X , x ] ⊙≃ ⊙[ X , y ]
+        homog-idf : fst (auto x) == ⊙idf ⊙[ X , x ]
+    open homogeneous public
+
+    homog-⊙Ω≃ : (y : X) → homogeneous → ⊙Ω ⊙[ X , x ] ⊙≃ ⊙Ω ⊙[ X , y ]
+    homog-⊙Ω≃ y (homog auto _) = ⊙Ω-emap (auto y)
+
+    homog-Ω≃ : (y : X) → homogeneous → (x == x) ≃ (y == y)
+    homog-Ω≃ y η = ⊙≃-to-≃ (homog-⊙Ω≃ y η)
+
+  {-
+    Two pointed homotopies of pointed maps valued in a coherently homogeneous
+    type are equal as soon as their underlying homotopies are equal.
+  -}
+  
+  module _ {j} {Z : Type j} {z : Z} {f : Z → X} where
+
+    ⊙∼-eval : ⊙[ f ∼ f , (λ z → idp) ] ⊙→ ⊙[ f z == f z , idp ]
+    fst ⊙∼-eval = λ H → H z
+    snd ⊙∼-eval = idp
+
+    ⊙∼-eval-sect : homogeneous (f z) → has-sect⊙ ⊙∼-eval
+    fst (has-sect⊙.r-inv (⊙∼-eval-sect η)) p = λ x₁ → –>(homog-Ω≃ (f z) (f x₁) η) p
+    snd (has-sect⊙.r-inv (⊙∼-eval-sect (homog auto _))) =
+      λ= λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+        !-inv-l (snd (fst (auto (f x))))
+    has-sect⊙.sect⊙-eq (⊙∼-eval-sect (homog auto homog-idf)) =
+      ⊙λ= (comp-to-⊙
+        ((λ x → app= (ap (fst ∘ ⊙Ω-fmap) homog-idf ∙ ap fst ⊙Ω-fmap-idf) x) ,
+        pathseq))
+      where
+        lemma : {m : ⊙[ X , f z ] ⊙→ ⊙[ X , f z ]} (τ : m == ⊙idf ⊙[ X , f z ]) 
+          → ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap) τ) ∙ idp) ∙
+            transport (λ v → Ω-fmap v idp == idp) (! τ) idp ∙ idp
+            == idp
+        lemma idp = idp
+
+        pathseq :
+          ! (ap (λ u → u idp)
+            (ap (fst ∘ ⊙Ω-fmap) homog-idf ∙
+            ap fst (pair= (λ= ap-idf)
+              (↓-app=cst-in (ap (_∙ idp) (! (app=-β ap-idf idp))))))) ∙
+          ap (λ H → H z) (λ= (λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+            !-inv-l (snd (fst (auto (f x)))))) ∙ idp
+          =-=
+          idp
+        pathseq = 
+          ! (ap (λ u → u idp)
+            (ap (fst ∘ ⊙Ω-fmap) homog-idf ∙
+            ap fst (pair= (λ= ap-idf) _))) ∙
+          ap (λ H → H z) (λ= (λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+            !-inv-l (snd (fst (auto (f x)))))) ∙ idp
+            =⟪ ap (λ p → ! p ∙ ap (λ H → H z)
+                   (λ= (λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+                   !-inv-l (snd (fst (auto (f x)))))) ∙ idp) (
+                 ap-∙ (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap) homog-idf)
+                   (ap fst (pair= (λ= ap-idf) _))) ⟫
+          ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap) homog-idf) ∙
+            ap (λ u → u idp) (ap fst (pair= (λ= ap-idf) _))) ∙
+          ap (λ H → H z) (λ= (λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+            !-inv-l (snd (fst (auto (f x)))))) ∙ idp
+            =⟪ ap (λ p → ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap)
+                    homog-idf) ∙ p) ∙ ap (λ H → H z)
+                    (λ= (λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+                    !-inv-l (snd (fst (auto (f x)))))) ∙ idp)
+                  (ap (ap (λ u → u idp)) (fst=-β (λ= ap-idf)
+                    (↓-app=cst-in (ap (_∙ idp) (! (app=-β ap-idf idp))))) ∙ λ=-ap-idf) ⟫
+          ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap)
+            homog-idf) ∙ idp) ∙
+          ap (λ H → H z) (λ= (λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+            !-inv-l (snd (fst (auto (f x)))))) ∙ idp
+          =⟪ ap (λ p → ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap)
+               homog-idf) ∙ idp) ∙ p ∙ idp) (
+               funext-nat-∼  z (λ x → Ω-fmap-β∙ (fst (auto (f x))) idp ∙
+               !-inv-l (snd (fst (auto (f x)))))) ⟫
+          ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap)
+            homog-idf) ∙ idp) ∙
+          (Ω-fmap-β∙ (fst (auto (f z))) idp ∙
+            !-inv-l (snd (fst (auto (f z))))) ∙ idp
+            =⟪ ap (λ p → ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap)
+               homog-idf) ∙ idp) ∙ p ∙ idp)
+               (! (apd-tr (λ F → Ω-fmap-β∙ F idp ∙ !-inv-l (snd F))
+               (! homog-idf))) ⟫
+          ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap)
+            homog-idf) ∙ idp) ∙
+          transport (λ v → Ω-fmap v idp == idp)
+            (! homog-idf) idp ∙ idp
+            =⟪ lemma homog-idf ⟫
+          idp ∎∎
+
+    ⊙∼-evalΩ-sect : homogeneous (f z) → has-sect⊙ (⊙Ω-fmap ⊙∼-eval)
+    ⊙∼-evalΩ-sect η = ⊙Ω-sect (⊙∼-eval) (⊙∼-eval-sect η)
+
+    module _ (η : homogeneous (f z)) where
+
+      open has-sect⊙
+
+      ∼⊙homog= : (x : X) {g : Z → X}
+        {fₚ : f z == x} {gₚ : g z == x}
+        {H₁ H₂ : f == g}
+        {H₁ₚ : ! (app= H₁ z) ∙ fₚ =-= gₚ}
+        {H₂ₚ : ! (app= H₂ z) ∙ fₚ =-= gₚ}
+        →  H₁ == H₂ → (app= H₁ , H₁ₚ) ⊙→∼ (app= H₂ , H₂ₚ)
+      fst (∼⊙homog= x {fₚ = idp} {H₁ = idp} {H₁ₚ = H₁ₚ} {H₂ₚ} idp) =
+        λ x₁ → app= (fst (r-inv (⊙∼-evalΩ-sect η))
+          (ap-post∙idp∘!-inv (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ))))) x₁
+      snd (∼⊙homog= x {fₚ = idp} {H₁ = idp} {H₁ₚ = H₁ₚ} {H₂ₚ} idp) =
+        post↯-rotate-in (=ₛ-in (ap (ap (λ p → ! p ∙ idp))
+        (app= (ap fst (sect⊙-eq (⊙∼-evalΩ-sect η)))
+          (ap-post∙idp∘!-inv (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ))))) ∙
+        <–-inv-r (ap-equiv (post∙idp∘!-is-equiv) idp idp)
+          (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ)))))
+
+      ∼⊙homog∼ : (x : X) {g : Z → X}
+        {fₚ : f z == x} {gₚ : g z == x}
+        {H₁ H₂ : f ∼ g}
+        {H₁ₚ : ! (H₁ z) ∙ fₚ =-= gₚ}
+        {H₂ₚ : ! (H₂ z) ∙ fₚ =-= gₚ}
+        →  H₁ ∼ H₂ → (H₁ , H₁ₚ) ⊙→∼ (H₂ , H₂ₚ)
+      fst (∼⊙homog∼ x {fₚ = idp} {gₚ} {H₁} {H₂} {H₁ₚ} {H₂ₚ} K) t =
+        ! (app=-β H₁ t) ∙
+        fst (∼⊙homog= x {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
+          {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
+          {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
+          (ap λ= (λ= K))) t ∙
+        app=-β H₂ t
+      snd (∼⊙homog∼ x {fₚ = idp} {gₚ} {H₁} {H₂} {H₁ₚ} {H₂ₚ} K) =
+        ap (λ p → ! p ∙ idp) (! (app=-β H₁ z) ∙
+          fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
+            {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
+            {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
+            (ap λ= (λ= K))) z ∙ app=-β H₂ z) ◃∙
+        H₂ₚ
+          =ₛ₁⟨ 0 & 1 & ap-!∙∙ (λ p → ! p ∙ idp) (app=-β H₁ z)
+               (fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
+                 {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
+                 {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
+                 (ap λ= (λ= K))) z) (app=-β H₂ z) ⟩
+        ↯ (! (ap (λ p → ! p ∙ idp) (app=-β H₁ z)) ◃∙
+         ap (λ p → ! p ∙ idp) (fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ}
+              {H₁ = λ= H₁} {H₂ = λ= H₂}
+              {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
+              {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
+              (ap λ= (λ= K))) z) ◃∙
+         ap (λ p → ! p ∙ idp) (app=-β H₂ z) ◃∎) ◃∙ H₂ₚ
+           =ₛ⟨ pre-rotate-in-↯-assoc
+                 (snd (∼⊙homog= x
+                 {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
+                 {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
+                 {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
+                 (ap λ= (λ= K)))) ⟩
+         H₁ₚ ∎ₛ
+
+-- All loop spaces are coherently homogeneous.
+
+module _ {i} {X : Type i} {x : X} where
+
+  module _ {p : x == x} where
+
+    loop-homog : homogeneous p
+    fst (fst (auto loop-homog q)) = λ ℓ → ℓ ∙ ! p ∙ q
+    snd (fst (auto loop-homog q)) =
+      ! (∙-assoc p (! p) q) ∙ ap (λ c → c ∙ q) (!-inv-r p)
+    snd (auto loop-homog q) = post∙-is-equiv (! p ∙ q)
+    homog-idf loop-homog =
+      ⊙λ= (comp-to-⊙ ((λ x₁ → ap (λ c → x₁ ∙ c) (!-inv-l p) ∙ ∙-unit-r x₁) ,
+        !-inv-l-r-unit-assoc p ◃∎))
+
+  ∼⊙Ωhomog∼ : ∀ {j} {Z : Ptd j} {p : x == x}
+    {f g : Z ⊙→ ⊙[ x == x , p ]}
+    {H₁ H₂ : fst f ∼ fst g}
+    {H₁ₚ : ! (H₁ (pt Z)) ∙ snd f =-= snd g}
+    {H₂ₚ : ! (H₂ (pt Z)) ∙ snd f =-= snd g}
+    →  H₁ ∼ H₂ → (H₁ , H₁ₚ) ⊙→∼ (H₂ , H₂ₚ)
+  ∼⊙Ωhomog∼ {Z = Z} {p} {f} K = ∼⊙homog∼ (loop-homog {p = fst f (pt Z)}) p K
diff --git a/HoTT-Agda/core/lib/types/LoopSpace.agda b/HoTT-Agda/core/lib/types/LoopSpace.agda
new file mode 100644
index 0000000..4568952
--- /dev/null
+++ b/HoTT-Agda/core/lib/types/LoopSpace.agda
@@ -0,0 +1,144 @@
+{-# OPTIONS --without-K --rewriting #-}
+
+open import lib.Basics
+open import lib.types.Pointed
+open import lib.types.Sigma
+
+module lib.types.LoopSpace where
+
+{- loop space -}
+
+module _ {i} where
+
+  ⊙Ω : Ptd i → Ptd i
+  ⊙Ω ⊙[ A , a ] = ⊙[ (a == a) , idp ]
+
+  Ω : Ptd i → Type i
+  Ω = de⊙ ∘ ⊙Ω
+
+module _ {i} {X : Ptd i} where
+
+  Ω-! : Ω X → Ω X
+  Ω-! = !
+
+  Ω-∙ : Ω X → Ω X → Ω X
+  Ω-∙ = _∙_
+
+{- pointed versions of functions on paths -}
+
+⊙Ω-∙ : ∀ {i} {X : Ptd i} → ⊙Ω X ⊙× ⊙Ω X ⊙→ ⊙Ω X
+⊙Ω-∙ = (uncurry Ω-∙ , idp)
+
+⊙Ω-fmap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
+  → X ⊙→ Y → ⊙Ω X ⊙→ ⊙Ω Y
+⊙Ω-fmap (f , idp) = ap f , idp
+
+Ω-fmap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
+  → X ⊙→ Y → (Ω X → Ω Y)
+Ω-fmap F = fst (⊙Ω-fmap F)
+
+Ω-fmap-β : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p : Ω X)
+  → Ω-fmap F p == ! (snd F) ∙ ap (fst F) p ∙' snd F
+Ω-fmap-β (_ , idp) _ = idp
+
+Ω-fmap-β∙ : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p : Ω X)
+  → Ω-fmap F p == ! (snd F) ∙ ap (fst F) p ∙ snd F
+Ω-fmap-β∙ (f , idp) p = ! (∙-unit-r (ap f p))
+
+Ω-fmap-pt-β : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y)
+  → snd (⊙Ω-fmap F) ==
+    Ω-fmap-β F idp ∙ ap (λ p → ! (snd F) ∙ p) (∙'-unit-l (snd F)) ∙ !-inv-l (snd F) 
+Ω-fmap-pt-β (_ , idp) = idp
+
+Ω-isemap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
+  (F : X ⊙→ Y) → is-equiv (fst F) → is-equiv (Ω-fmap F)
+Ω-isemap (f , idp) e = ap-is-equiv e _ _
+
+Ω-emap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
+  → (X ⊙≃ Y) → (Ω X ≃ Ω Y)
+Ω-emap (F , F-is-equiv) = Ω-fmap F , Ω-isemap F F-is-equiv
+
+⊙Ω-emap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
+  → (X ⊙≃ Y) → (⊙Ω X ⊙≃ ⊙Ω Y)
+⊙Ω-emap (F , F-is-equiv) = ⊙Ω-fmap F , Ω-isemap F F-is-equiv
+
+⊙Ω-fmap2 : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
+  → X ⊙× Y ⊙→ Z → ⊙Ω X ⊙× ⊙Ω Y ⊙→ ⊙Ω Z
+⊙Ω-fmap2 (f , idp) = (λ{(p , q) → ap2 (curry f) p q}) , idp
+
+⊙Ω-fmap-∘ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
+  (g : Y ⊙→ Z) (f : X ⊙→ Y)
+  → ⊙Ω-fmap (g ⊙∘ f) == ⊙Ω-fmap g ⊙∘ ⊙Ω-fmap f
+⊙Ω-fmap-∘ (g , idp) (f , idp) = ⊙λ=' (λ p → ap-∘ g f p) idp
+
+⊙Ω-csmap : ∀ {i₀ i₁ j₀ j₁} {X₀ : Ptd i₀} {X₁ : Ptd i₁}
+  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
+  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
+  → ⊙CommSquare f g hX hY
+  → ⊙CommSquare (⊙Ω-fmap f) (⊙Ω-fmap g) (⊙Ω-fmap hX) (⊙Ω-fmap hY)
+⊙Ω-csmap {f = f} {g} {hX} {hY} (⊙comm-sqr cs) = ⊙comm-sqr $ ⊙app= $
+  ⊙Ω-fmap hY ⊙∘ ⊙Ω-fmap f
+    =⟨ ! $ ⊙Ω-fmap-∘ hY f ⟩
+  ⊙Ω-fmap (hY ⊙∘ f)
+    =⟨ ap ⊙Ω-fmap $ ⊙λ= cs ⟩
+  ⊙Ω-fmap (g ⊙∘ hX)
+    =⟨ ⊙Ω-fmap-∘ g hX ⟩
+  ⊙Ω-fmap g ⊙∘ ⊙Ω-fmap hX
+    =∎
+
+⊙Ω-csemap : ∀ {i₀ i₁ j₀ j₁} {X₀ : Ptd i₀} {X₁ : Ptd i₁}
+  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
+  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
+  → ⊙CommSquareEquiv f g hX hY
+  → ⊙CommSquareEquiv (⊙Ω-fmap f) (⊙Ω-fmap g) (⊙Ω-fmap hX) (⊙Ω-fmap hY)
+⊙Ω-csemap {f = f} {g} {hX} {hY} (⊙comm-sqr cs , hX-ise , hY-ise) =
+  (⊙comm-sqr $ ⊙app= $
+    ⊙Ω-fmap hY ⊙∘ ⊙Ω-fmap f
+      =⟨ ! $ ⊙Ω-fmap-∘ hY f ⟩
+    ⊙Ω-fmap (hY ⊙∘ f)
+      =⟨ ap ⊙Ω-fmap $ ⊙λ= cs ⟩
+    ⊙Ω-fmap (g ⊙∘ hX)
+      =⟨ ⊙Ω-fmap-∘ g hX ⟩
+    ⊙Ω-fmap g ⊙∘ ⊙Ω-fmap hX
+      =∎) ,
+  Ω-isemap hX hX-ise , Ω-isemap hY hY-ise
+
+⊙Ω-fmap-idf : ∀ {i} {X : Ptd i} → ⊙Ω-fmap (⊙idf X) == ⊙idf _
+⊙Ω-fmap-idf = ⊙λ=' ap-idf idp
+
+⊙Ω-sect : ∀ {i j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
+  → has-sect⊙ f → has-sect⊙ (⊙Ω-fmap f)
+has-sect⊙.r-inv (⊙Ω-sect f (sect⊙ r-inv sect⊙-eq)) = ⊙Ω-fmap r-inv
+has-sect⊙.sect⊙-eq (⊙Ω-sect f (sect⊙ r-inv sect⊙-eq)) =
+  ! (! (ap (⊙Ω-fmap) sect⊙-eq ∙ ⊙Ω-fmap-idf) ∙ ⊙Ω-fmap-∘ f r-inv)
+
+⊙Ω-fmap2-fst : ∀ {i j} {X : Ptd i} {Y : Ptd j}
+  → ⊙Ω-fmap2 {X = X} {Y = Y} ⊙fst == ⊙fst
+⊙Ω-fmap2-fst = ⊙λ=' (uncurry ap2-fst) idp
+
+⊙Ω-fmap2-snd : ∀ {i j} {X : Ptd i} {Y : Ptd j}
+  → ⊙Ω-fmap2 {X = X} {Y = Y} ⊙snd == ⊙snd
+⊙Ω-fmap2-snd = ⊙λ=' (uncurry ap2-snd) idp
+
+⊙Ω-fmap-fmap2 : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
+  (G : Z ⊙→ W) (F : X ⊙× Y ⊙→ Z)
+  → ⊙Ω-fmap G ⊙∘ ⊙Ω-fmap2 F == ⊙Ω-fmap2 (G ⊙∘ F)
+⊙Ω-fmap-fmap2 (g , idp) (f , idp) =
+  ⊙λ=' (uncurry (ap-ap2 g (curry f))) idp
+
+⊙Ω-fmap2-fmap : ∀ {i j k l m}
+  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
+  (G : (U ⊙× V) ⊙→ Z) (F₁ : X ⊙→ U) (F₂ : Y ⊙→ V)
+  → ⊙Ω-fmap2 G ⊙∘ ⊙×-fmap (⊙Ω-fmap F₁) (⊙Ω-fmap F₂) == ⊙Ω-fmap2 (G ⊙∘ ⊙×-fmap F₁ F₂)
+⊙Ω-fmap2-fmap (g , idp) (f₁ , idp) (f₂ , idp) =
+  ⊙λ=' (λ {(p , q) → ap2-ap-l (curry g) f₁ p (ap f₂ q)
+                   ∙ ap2-ap-r (λ x v → g (f₁ x , v)) f₂ p q})
+       idp
+
+⊙Ω-fmap2-diag : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙× X ⊙→ Y)
+  → ⊙Ω-fmap2 F ⊙∘ ⊙diag == ⊙Ω-fmap (F ⊙∘ ⊙diag)
+⊙Ω-fmap2-diag (f , idp) = ⊙λ=' (ap2-diag (curry f)) idp
+
+Ω-fmap-∙ : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p q : Ω X)
+  → Ω-fmap F (p ∙ q) == Ω-fmap F p ∙ Ω-fmap F q
+Ω-fmap-∙ (f , idp) p q = ap-∙ f p q
diff --git a/HoTT-Agda/core/lib/types/Paths.agda b/HoTT-Agda/core/lib/types/Paths.agda
index e6b127c..f3b81ca 100644
--- a/HoTT-Agda/core/lib/types/Paths.agda
+++ b/HoTT-Agda/core/lib/types/Paths.agda
@@ -62,6 +62,31 @@ module _ {i} {A : Type i} {x y z : A} where
   post∙'-equiv : (p : y == z) → (x == y) ≃ (x == z)
   post∙'-equiv p = ((λ q → q ∙' p) , post∙'-is-equiv p)
 
+module _ {i} {A : Type i} {x y : A} where
+
+  post∙idp∘!-is-equiv : (x == y) ≃ (y == x) 
+  post∙idp∘!-is-equiv = (post∙-equiv idp) ∘e (!-equiv)
+
+  ap-post∙idp∘!-inv : {p₁ p₂ : x == y}
+    → (! p₁ ∙ idp == ! p₂ ∙ idp) → p₁ == p₂
+  ap-post∙idp∘!-inv {p₁} {p₂} = <– (ap-equiv (post∙idp∘!-is-equiv) p₁ p₂)
+
+
+module _ {i j} {A : Type i} {B : Type j} {f g : A → B} where
+
+  funext-nat : (a : A) {H₁ H₂ : f ∼ g} (K : H₁ == H₂)
+    → ap (λ H → H a) K == app= K a
+  funext-nat a idp = idp
+
+  funext-nat-∼ : (a : A) {H₁ H₂ : f ∼ g} (K : H₁ ∼ H₂)
+    → ap (λ H → H a) (λ= K) == K a
+  funext-nat-∼ a K = funext-nat a (λ= K) ∙ app=-β K a
+
+module _ {i} {A : Type i} {a : A} where
+
+  λ=-ap-idf : ap (λ H → H (idp :> (a == a))) (λ= (ap-idf {A = A})) == idp
+  λ=-ap-idf = funext-nat-∼ idp ap-idf
+
 module _ {i j} {A : Type i} {B : Type j}
   {f : A → B} {x y : A} {b : B} where
 
@@ -290,37 +315,3 @@ module _ {i j} {A : Type i} {B : Type j} (g : B → A) (f : A → B) where
     → ((ap g (ap f p) ∙' v) == (u ∙ p))
     → (u == v [ (λ x → g (f x) == x) ↓ p ])
   ↓-∘=idf-in' {p = idp} q = ! (∙-unit-r _) ∙ (! q) ∙ (∙'-unit-l _)
-
--- WIP, derive it from more primitive principles
--- ↓-∘=id-in f g {p = p} {u} {v} q =
---   ↓-=-in (u ◃ apd (λ x → g (f x)) p =⟨ apd-∘ f g p |in-ctx (λ t → u ◃ t) ⟩
---         u ◃ ↓-apd-out _ f p (apdd g p (apd f p)) =⟨ apdd-cst (λ _ b → g b) p (ap f p) (! (apd-nd f p)) |in-ctx (λ t → u ◃ ↓-apd-out _ f p t) ⟩
---         u ◃ ↓-apd-out _ f p (apd (λ t → g (π₂ t)) (pair= p (apd f p))) =⟨ apd-∘ π₂ g (pair= p (apd f p)) |in-ctx (λ t → u ◃ ↓-apd-out _ f p t) ⟩
---         u ◃ ↓-apd-out _ f p (↓-apd-out _ π₂ (pair= p (apd f p)) (apdd g (pair= p (apd f p)) (apd π₂ (pair= p (apd f p))))) =⟨ {!!} ⟩
---         apd (λ x → x) p ▹ v ∎)
-
--- module _ {i j} {A : Type i} {B : Type j} {x y z : A → B} where
-
---   lhs :
---     {a a' : A} {p : a == a'} {q : x a == y a} {q' : x a' == y a'}
---     {r : y a == z a} {r' : y a' == z a'}
---     (α : q == q'            [ (λ a → x a == y a) ↓ p ])
---     (β : r ∙ ap z p == ap y p ∙' r')
---     → (q ∙' r) ∙ ap z p == ap x p ∙' q' ∙' r'
---   lhs =
---     (q ∙' r) ∙ ap z p     =⟨ ? ⟩  -- assoc
---     q ∙' (r ∙ ap z p)     =⟨ ? ⟩  -- β
---     q ∙' (ap y p ∙' r')   =⟨ ? ⟩  -- assoc
---     (q ∙' ap y p) ∙' r'   =⟨ ? ⟩  -- ∙ = ∙'
---     (q ∙ ap y p) ∙' r'    =⟨ ? ⟩  -- α
---     (ap x p ∙' q') ∙' r'  =⟨ ? ⟩  -- assoc
---     ap x p ∙' q' ∙' r' ∎
-
-
---   thing :
---     {a a' : A} {p : a == a'} {q : x a == y a} {q' : x a' == y a'}
---     {r : y a == z a} {r' : y a' == z a'}
---     (α : q == q'            [ (λ a → x a == y a) ↓ p ])
---     (β : r ∙ ap z p == ap y p ∙' r')
---     → (_∙'2ᵈ_ {r = r} {r' = r'} α (↓-='-in' β) == ↓-='-in' {!!})
---   thing = {!!}
diff --git a/HoTT-Agda/core/lib/types/Pointed.agda b/HoTT-Agda/core/lib/types/Pointed.agda
index efde1de..ee58a71 100644
--- a/HoTT-Agda/core/lib/types/Pointed.agda
+++ b/HoTT-Agda/core/lib/types/Pointed.agda
@@ -54,6 +54,81 @@ module lib.types.Pointed where
   → (f : Y ⊙→ Z) → f ⊙∘ (⊙cst :> (X ⊙→ Y)) ⊙∼ ⊙cst
 ⊙∘-cst-r {X = X} f = (λ _ → snd f) , ↓-idf=cst-in' idp
 
+module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} where 
+
+  ⊙∘-assoc-comp : ∀ {l} {W : Ptd l} (h : Z ⊙→ W) (g : Y ⊙→ Z) (f : X ⊙→ Y)
+    → ((h ⊙∘ g) ⊙∘ f) ⊙-comp (h ⊙∘ (g ⊙∘ f))
+  fst (⊙∘-assoc-comp (h , hpt) (g , gpt) (f , fpt)) = λ x → idp
+  snd (⊙∘-assoc-comp (h , hpt) (g , gpt) (f , fpt)) =
+    ! (∙-assoc (ap (h ∘ g) fpt) (ap h gpt) hpt) ◃∙
+    ap (λ p → p ∙ hpt) (ap (λ p → p ∙ ap h gpt) (ap-∘ h g fpt)) ◃∙
+    ap (λ p → p ∙ hpt) (∙-ap h (ap g fpt) gpt) ◃∎
+
+-- pre- and post-comp on (unfolded) homotopies of pointed maps
+
+  ⊙∘-post : {f₁ f₂ : X ⊙→ Y} (g : Y ⊙→ Z) (H : f₁ ⊙-comp f₂) → g ⊙∘ f₁ ⊙-comp g ⊙∘ f₂
+  fst (⊙∘-post g H) = λ x → ap (fst g) (fst H x)
+  snd (⊙∘-post {f₁} g H) =
+    ! (∙-assoc (! (ap (fst g) (fst H (pt X)))) (ap (fst g) (snd f₁)) (snd g)) ◃∙
+    ap (λ p → p ∙ snd g) (!-ap-∙ (fst g) (fst H (pt X)) (snd f₁)) ◃∙
+    ap (λ p → p ∙ snd g) (ap (ap (fst g)) (↯ (snd H))) ◃∎
+
+  ⊙∘-pre : {f₁ f₂ : X ⊙→ Y} (g : Z ⊙→ X) (H : f₁ ⊙-comp f₂) → f₁ ⊙∘ g ⊙-comp f₂ ⊙∘ g
+  fst (⊙∘-pre g H) = λ x → fst H (fst g x)
+  snd (⊙∘-pre {f₁} {f₂} g H) =
+    ! (∙-assoc (! (fst H (fst g (pt Z)))) (ap (fst f₁) (snd g)) (snd f₁)) ◃∙
+    ap (λ p → p ∙ snd f₁) (hmtpy-nat-!-sq (fst H) (snd g)) ◃∙
+    ∙-assoc (ap (fst f₂) (snd g)) (! (fst H (pt X))) (snd f₁) ◃∙
+    ap (λ p → ap (fst f₂) (snd g) ∙ p) (↯ (snd H)) ◃∎
+
+-- concatenation of homotopies of pointed maps
+
+module _ {i j} {X : Ptd i} {Y : Ptd j} {f₁ f₂ f₃ : X ⊙→ Y} where 
+
+  infixr 15 _∙⊙∼_
+  _∙⊙∼_ : f₁ ⊙-comp f₂ → f₂ ⊙-comp f₃ → f₁ ⊙-comp f₃
+  fst (H₁ ∙⊙∼ H₂) = λ x → fst H₁ x ∙ fst H₂ x 
+  snd (H₁ ∙⊙∼ H₂) =
+    ap (λ p → ! (p ∙ fst H₂ (pt X)) ∙ snd f₁) (tri-exch (↯ (snd H₁))) ◃∙ 
+    ap (λ p → ! ((snd f₁ ∙ ! (snd f₂)) ∙ p) ∙ snd f₁) (tri-exch (↯ (snd H₂))) ◃∙
+    !3-∙3 (snd f₁) (snd f₂) (snd f₃) ◃∎
+
+-- inverse of homotopy of pointed maps
+
+module _ {i j} {X : Ptd i} {Y : Ptd j} where
+
+  !-⊙∼ : {f₁ f₂ : X ⊙→ Y} (H : f₁ ⊙-comp f₂) → f₂ ⊙-comp f₁
+  fst (!-⊙∼ (H₀ , H₁)) x = ! (H₀ x)
+  snd (!-⊙∼ {f₁} {f₂} (H₀ , H₁)) =
+    ap (λ p → p ∙ snd f₂) (!-! (H₀ (pt (X)))) ◃∙
+    ap (λ p → H₀ (pt X) ∙ p) (↯ (seq-! H₁)) ◃∙
+    ! (∙-assoc (H₀ (pt X)) (! (H₀ (pt X))) (snd f₁)) ◃∙
+    ap (λ p → p ∙ snd f₁) (!-inv-r (H₀ (pt X))) ◃∎
+
+-- identity homotopy of pointed maps
+
+  ⊙∼-id : (f : X ⊙→ Y) → f ⊙-comp f
+  fst (⊙∼-id (f , fₚ)) x = idp
+  snd (⊙∼-id (f , fₚ)) = idp ◃∎
+
+-- homotopies of homotopies of pointed maps
+
+module _ {i j} {X : Ptd i} {Y : Ptd j} where
+
+  infixr 10 _⊙→∼_
+  _⊙→∼_ : {f g : X ⊙→ Y} (H₁ H₂ : f ⊙-comp g) → Type (lmax i j)
+  _⊙→∼_ {f = f} H₁ H₂ =
+    Σ (fst H₁ ∼ fst H₂)
+      (λ K → ap (λ p →  ! p ∙ snd f) (K (pt X)) ◃∙ snd H₂ =ₛ snd H₁)
+
+-- pointed sections
+
+  record has-sect⊙ (f : X ⊙→ Y) : Type (lmax i j) where
+    constructor sect⊙
+    field
+      r-inv : Y ⊙→ X
+      sect⊙-eq : f ⊙∘ r-inv == ⊙idf Y
+
 {- Pointed equivalences -}
 
 -- Extracting data from an pointed equivalence
diff --git a/HoTT-Agda/core/lib/types/Suspension.agda b/HoTT-Agda/core/lib/types/Suspension.agda
new file mode 100644
index 0000000..55d33d3
--- /dev/null
+++ b/HoTT-Agda/core/lib/types/Suspension.agda
@@ -0,0 +1,179 @@
+{-# OPTIONS --without-K --rewriting --overlapping-instances #-}
+
+open import lib.Basics
+open import lib.types.Span
+open import lib.types.Pointed
+open import lib.types.Pushout
+open import lib.types.Unit
+open import lib.types.Paths
+
+-- Suspension is defined as a particular case of pushout
+
+module lib.types.Suspension where
+
+module _ {i} (A : Type i) where
+
+  susp-span : Span
+  susp-span = span Unit Unit A (λ _ → tt) (λ _ → tt)
+
+  Susp : Type i
+  Susp = Pushout susp-span
+
+  -- [north'] and [south'] explictly ask for [A]
+
+  north' : Susp
+  north' = left tt
+
+  south' : Susp
+  south' = right tt
+
+module _ {i} {A : Type i} where
+
+  north : Susp A
+  north = north' A
+
+  south : Susp A
+  south = south' A
+
+  merid : A → north == south
+  merid x = glue x
+
+  module SuspElim {j} {P : Susp A → Type j} (n : P north)
+    (s : P south) (p : (x : A) → n == s [ P ↓ merid x ]) where
+    open module P = PushoutElim (λ _ → n) (λ _ → s) p
+      public using (f) renaming (glue-β to merid-β)
+
+  open SuspElim public using () renaming (f to Susp-elim)
+
+  module SuspRec {j} {C : Type j} (n s : C) (p : A → n == s) where
+    open module P = PushoutRec {d = susp-span A} (λ _ → n) (λ _ → s) p
+      public using (f) renaming (glue-β to merid-β)
+
+  open SuspRec public using () renaming (f to Susp-rec)
+
+susp-⊙span : ∀ {i} → Ptd i → ⊙Span
+susp-⊙span X =
+  ⊙span ⊙Unit ⊙Unit X (⊙cst {X = X}) (⊙cst {X = X})
+
+⊙Susp : ∀ {i} → Ptd i → Ptd i
+⊙Susp ⊙[ A , _ ] = ⊙[ Susp A , north ]
+
+σloop : ∀ {i} (X : Ptd i) → de⊙ X → north' (de⊙ X) == north' (de⊙ X)
+σloop ⊙[ _ , x₀ ] x = merid x ∙ ! (merid x₀)
+
+σloop-pt : ∀ {i} {X : Ptd i} → σloop X (pt X) == idp
+σloop-pt {X = ⊙[ _ , x₀ ]} = !-inv-r (merid x₀)
+
+⊙σloop : ∀ {i} (X : Ptd i) → X ⊙→ ⊙[ north' (de⊙ X) == north' (de⊙ X) , idp ]
+⊙σloop X = σloop X , σloop-pt
+
+module _ {i j} {A : Type i} {B : Type j} (f g : Susp A → B)
+  (n : f north == g north) (s : f south == g south)
+  (c : (a : A) → ap f (merid a) =-= n ∙ ap g (merid a) ∙' ! s) where
+
+  SuspMapEq : f ∼ g
+  SuspMapEq = Susp-elim n s λ a → from-hmpty-nat f g (merid a) (↯ (c a))
+
+  SuspMapEq-β : (a : A) → hmpty-nat-∙'-r SuspMapEq (merid a) == ↯ (c a)
+  SuspMapEq-β a =
+    apd-to-hnat f g SuspMapEq (merid a) (↯ (c a))
+      (SuspElim.merid-β n s (λ z → from-hmpty-nat f g (merid z) (↯ (c z))) a)
+
+  SuspMapEq-!-β : (a : A) →
+   hmpty-nat-∙'-r SuspMapEq (! (merid a))
+   ==
+   ap-! f (merid a) ∙ ap ! (↯ (c a)) ∙ !-∙-ap-∙'-! g n (merid a) s
+  SuspMapEq-!-β a = apd-to-hnat-! f g SuspMapEq (merid a) (SuspMapEq-β a)
+
+  SuspMapEq-β-∙ : (a b : A) →
+    hmpty-nat-∙'-r SuspMapEq (merid a ∙ ! (merid b))
+    ==
+    ap-∙ f (merid a) (! (merid b)) ∙
+    ap (λ p → p ∙ ap f (! (merid b))) (↯ (c a)) ∙
+    ap (_∙_ (SuspMapEq north ∙ ap g (merid a) ∙' ! (SuspMapEq south)))
+      (ap-! f (merid b) ∙ ap ! (↯ (c b)) ∙ !-∙-ap-∙'-! g n (merid b) s) ∙
+    assoc-tri-!-mid (SuspMapEq north) (ap g (merid a)) (SuspMapEq south)
+      (ap g (! (merid b))) (! (SuspMapEq north)) ∙
+    ap (λ p → SuspMapEq north ∙ p ∙' ! (SuspMapEq north))
+      (! (ap-∙ g (merid a) (! (merid b))))
+  SuspMapEq-β-∙ a b =
+    apd-to-hnat-∙ f g SuspMapEq (merid a) (! (merid b)) (SuspMapEq-β a) (SuspMapEq-!-β b)
+
+  SuspMapEq-β-∙-ap! : ∀ {l} {C : Type l} (k : B → C) (a b : A) →
+    hmpty-nat-∙'-r (λ z → ap k (! (SuspMapEq z))) (merid a ∙ ! (merid b))
+    ==
+    ap-∘-long k g f SuspMapEq (merid a ∙ ! (merid b)) ∙
+    ! (ap (λ q → ap k (! (SuspMapEq north)) ∙ ap k q ∙' ! (ap k (! (SuspMapEq north))))
+      (ap-∙ f (merid a) (! (merid b)) ∙ ap (λ p → p ∙ ap f (! (merid b))) (↯ (c a)) ∙
+      ap (_∙_ (SuspMapEq north ∙ ap g (merid a) ∙' ! (SuspMapEq south)))
+      (ap-! f (merid b) ∙ ap ! (↯ (c b)) ∙ !-∙-ap-∙'-! g n (merid b) s) ∙
+      assoc-tri-!-mid (SuspMapEq north) (ap g (merid a))
+      (SuspMapEq south) (ap g (! (merid b))) (! (SuspMapEq north)) ∙
+      ap (λ p → SuspMapEq north ∙ p ∙' ! (SuspMapEq north))
+      (! (ap-∙ g (merid a) (! (merid b)))))) ∙
+    ! (ap (λ q → ap k (! (SuspMapEq north)) ∙ q ∙' ! (ap k (! (SuspMapEq north))))
+      (ap-∘ k f (merid a ∙ ! (merid b))))
+  SuspMapEq-β-∙-ap! k a b = apd-to-hnat-ap! f g SuspMapEq k (merid a ∙ ! (merid b)) (SuspMapEq-β-∙ a b)
+
+module _ {i j} where
+
+  module SuspFmap {A : Type i} {B : Type j} (f : A → B) =
+    SuspRec north south (merid ∘ f)
+
+  Susp-fmap : {A : Type i} {B : Type j} (f : A → B)
+    → (Susp A → Susp B)
+  Susp-fmap = SuspFmap.f
+
+  ⊙Susp-fmap : {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
+    → ⊙Susp X ⊙→ ⊙Susp Y
+  ⊙Susp-fmap (f , fpt) = (Susp-fmap f , idp)
+
+module _ {i} where
+
+  Susp-fmap-idf : (A : Type i) → ∀ a → Susp-fmap (idf A) a == a
+  Susp-fmap-idf A = Susp-elim idp idp $ λ a →
+    ↓-='-in' (ap-idf (merid a) ∙ ! (SuspFmap.merid-β (idf A) a))
+
+  ⊙Susp-fmap-idf : (X : Ptd i)
+    → ⊙Susp-fmap (⊙idf X) == ⊙idf (⊙Susp X)
+  ⊙Susp-fmap-idf X = ⊙λ=' (Susp-fmap-idf (de⊙ X)) idp
+
+module _ {i j k} where
+
+  Susp-fmap-∘ : {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B) (a : A)
+    → ap (Susp-fmap (g ∘ f)) (merid a) =-= ap (Susp-fmap g ∘ Susp-fmap f) (merid a)
+  Susp-fmap-∘ g f =
+    λ a → 
+      ap (Susp-fmap (g ∘ f)) (merid a)
+        =⟪ SuspFmap.merid-β (g ∘ f) a ⟫
+      merid (g (f a))
+        =⟪ ! (SuspFmap.merid-β g (f a)) ⟫
+      ap (Susp-fmap g) (merid (f a))
+        =⟪ ! (ap (ap (Susp-fmap g)) (SuspFmap.merid-β f a)) ⟫
+      ap (Susp-fmap g) (ap (Susp-fmap f) (merid a))
+        =⟪ ! (ap-∘ (Susp-fmap g) (Susp-fmap f) (merid a)) ⟫
+      ap (Susp-fmap g ∘ Susp-fmap f) (merid a) ∎∎ 
+
+module _ {i j k} {X : Type i} {Y : Type j} {Z : Type k} (g : Y → Z) (f : X → Y) where
+
+  Susp-fmap-∘-∼ =
+    SuspMapEq (Susp-fmap (g ∘ f)) (Susp-fmap g ∘ Susp-fmap f) idp idp
+      (Susp-fmap-∘ g f)
+
+module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} (g : Y ⊙→ Z) (f : X ⊙→ Y) where
+
+  ⊙Susp-fmap-∘ : ⊙Susp-fmap (g ⊙∘ f) == ⊙Susp-fmap g ⊙∘ ⊙Susp-fmap f
+  ⊙Susp-fmap-∘ = ⊙λ=' (Susp-fmap-∘-∼ (fst g) (fst f)) idp
+
+{- Extract the 'glue component' of a pushout -}
+module _ {i j k} {s : Span {i} {j} {k}} where
+
+  module ExtractGlue = PushoutRec {d = s} {D = Susp (Span.C s)}
+    (λ _ → north) (λ _ → south) merid
+
+  extract-glue = ExtractGlue.f
+
+  module _ {x₀ : Span.A s} where
+
+    ⊙extract-glue : ⊙[ Pushout s , left x₀ ] ⊙→ ⊙[ Susp (Span.C s) , north ]
+    ⊙extract-glue = extract-glue , idp
diff --git a/HoTT-Agda/hott-theorems.agda-lib b/HoTT-Agda/hott-theorems.agda-lib
new file mode 100644
index 0000000..d3cfd68
--- /dev/null
+++ b/HoTT-Agda/hott-theorems.agda-lib
@@ -0,0 +1,3 @@
+name: hott-theorems-modified
+depend: hott-core-modified
+include: theorems
\ No newline at end of file
diff --git a/HoTT-Agda/theorems/homotopy/PtdAdjoint.agda b/HoTT-Agda/theorems/homotopy/PtdAdjoint.agda
new file mode 100644
index 0000000..27dc301
--- /dev/null
+++ b/HoTT-Agda/theorems/homotopy/PtdAdjoint.agda
@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K --rewriting #-}
+
+open import lib.Basics
+open import lib.types.Pointed
+
+{- The pseudo-adjoint functors F,G : Ptd → Ptd
+ - It stops at composition and ignores
+ - all the higher associahedrons.
+ -}
+
+module homotopy.PtdAdjoint where
+
+record PtdFunctor i j : Type (lsucc (lmax i j)) where
+  field
+    obj : Ptd i → Ptd j
+    arr : {X Y : Ptd i} → X ⊙→ Y → obj X ⊙→ obj Y
+    id : (X : Ptd i) → arr (⊙idf X) == ⊙idf (obj X)
+    comp : {X Y Z : Ptd i} (g : Y ⊙→ Z) (f : X ⊙→ Y)
+      → arr (g ⊙∘ f) == arr g ⊙∘ arr f
+
+{- counit-unit description of F ⊣ G -}
+record CounitUnitAdjoint {i j} (F : PtdFunctor i j) (G : PtdFunctor j i)
+  : Type (lsucc (lmax i j)) where
+
+  private
+    module F = PtdFunctor F
+    module G = PtdFunctor G
+
+  field
+    η : (X : Ptd i) → (X ⊙→ G.obj (F.obj X))
+    ε : (U : Ptd j) → (F.obj (G.obj U) ⊙→ U)
+
+    η-natural : {X Y : Ptd i} (h : X ⊙→ Y)
+      → η Y ⊙∘ h == G.arr (F.arr h) ⊙∘ η X
+    ε-natural : {U V : Ptd j} (k : U ⊙→ V)
+      → ε V ⊙∘ F.arr (G.arr k) == k ⊙∘ ε U
+
+    εF-Fη : (X : Ptd i) → ε (F.obj X) ⊙∘ F.arr (η X) == ⊙idf (F.obj X)
+    Gε-ηG : (U : Ptd j) → G.arr (ε U) ⊙∘ η (G.obj U) == ⊙idf (G.obj U)
+
+{- hom-set isomorphism description of F ⊣ G -}
+record HomAdjoint {i j} (F : PtdFunctor i j) (G : PtdFunctor j i)
+  : Type (lsucc (lmax i j)) where
+
+  private
+    module F = PtdFunctor F
+    module G = PtdFunctor G
+
+  field
+    eq : (X : Ptd i) (U : Ptd j) → (F.obj X ⊙→ U) ≃ (X ⊙→ G.obj U)
+
+    nat-dom : {X Y : Ptd i} (h : X ⊙→ Y) (U : Ptd j)
+      (r : F.obj Y ⊙→ U)
+      → –> (eq Y U) r ⊙∘ h == –> (eq X U) (r ⊙∘ F.arr h)
+
+    nat-cod : (X : Ptd i) {U V : Ptd j} (k : U ⊙→ V)
+      (r : F.obj X ⊙→ U)
+      → G.arr k ⊙∘ –> (eq X U) r == –> (eq X V) (k ⊙∘ r)
+
+  nat!-dom : {X Y : Ptd i} (h : X ⊙→ Y) (U : Ptd j)
+    (s : Y ⊙→ G.obj U)
+    → <– (eq Y U) s ⊙∘ F.arr h == <– (eq X U) (s ⊙∘ h)
+  nat!-dom {X} {Y} h U s =
+    ! (<–-inv-l (eq X U) (<– (eq Y U) s ⊙∘ F.arr h))
+    ∙ ap (<– (eq X U)) (! (nat-dom h U (<– (eq Y U) s)))
+    ∙ ap (λ w → <– (eq X U) (w ⊙∘ h)) (<–-inv-r (eq Y U) s)
+
+  nat!-cod : (X : Ptd i) {U V : Ptd j} (k : U ⊙→ V)
+    (s : X ⊙→ G.obj U)
+    → k ⊙∘ <– (eq X U) s == <– (eq X V) (G.arr k ⊙∘ s)
+  nat!-cod X {U} {V} k s =
+    ! (<–-inv-l (eq X V) (k ⊙∘ <– (eq X U) s))
+    ∙ ap (<– (eq X V)) (! (nat-cod X k (<– (eq X U) s)))
+    ∙ ap (λ w → <– (eq X V) (G.arr k ⊙∘ w)) (<–-inv-r (eq X U) s)
diff --git a/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda b/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda
new file mode 100644
index 0000000..0df4482
--- /dev/null
+++ b/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda
@@ -0,0 +1,642 @@
+{-# OPTIONS --without-K --rewriting #-}
+
+open import lib.Basics
+open import lib.types.Pointed
+open import lib.types.Pushout
+open import lib.types.Suspension
+open import lib.types.LoopSpace
+open import lib.types.Homogeneous
+open import homotopy.PtdAdjoint
+
+module homotopy.SuspAdjointLoop where
+
+module _ {i} where
+
+  SuspFunctor : PtdFunctor i i
+  SuspFunctor = record {
+    obj = ⊙Susp;
+    arr = ⊙Susp-fmap;
+    id = ⊙Susp-fmap-idf;
+    comp = ⊙Susp-fmap-∘}
+
+  LoopFunctor : PtdFunctor i i
+  LoopFunctor = record {
+    obj = ⊙Ω;
+    arr = ⊙Ω-fmap;
+    id = λ _ → ⊙Ω-fmap-idf;
+    comp = ⊙Ω-fmap-∘}
+
+  -- counit
+
+  module _ (X : Ptd i) where
+
+    η : de⊙ X → Ω (⊙Susp X)
+    η x = σloop X x
+
+    ⊙η : X ⊙→ ⊙Ω (⊙Susp X)
+    ⊙η = (η , σloop-pt)
+
+-- induced map of hom types
+
+module _ {i j} (X : Ptd i) (U : Ptd j) where
+
+  into : ⊙Susp X ⊙→ U → X ⊙→ ⊙Ω U
+  into r = ⊙Ω-fmap r ⊙∘ ⊙η X
+
+  ap-comp-into-coher-aux : {f g : Susp (de⊙ X) → de⊙ U} (H₀ : f ∼ g)
+    {x : Susp (de⊙ X)} (v : x == right unit)
+    → ! (
+        (hmpty-nat-∙'-r H₀ (v ∙ ! v) ∙
+          ap (λ p → p ∙ ap g (v ∙ ! v) ∙' ! (H₀ x))
+            (! (!-! (H₀ x)) ∙ ! (!-∙ (! (H₀ x)) idp)) ∙
+          ap (λ p → ! (! (H₀ x) ∙ idp) ∙ ap g (v ∙ ! v) ∙' p)
+            (! (∙-unit-r (! (H₀ x)))) ∙ idp) ∙
+        ! (Ω-fmap-β (g , ! (H₀ x) ∙ idp)  (v ∙ ! v))) ∙
+      ap (ap f) (!-inv-r v) ∙ idp
+      =-=
+      ap (fst (⊙Ω-fmap (g , ! (H₀ x) ∙ idp))) (!-inv-r v) ∙
+      snd (⊙Ω-fmap (g , ! (H₀ x) ∙ idp))
+  ap-comp-into-coher-aux {g = g} H₀ idp = lemma (H₀ (right unit))
+    where
+      lemma : {x : de⊙ U} (u : x == g (right unit))
+        → ! (
+          ((! (!-inv-r u) ∙
+          ap (_∙_ u) (! (∙'-unit-l (! u)))) ∙
+          ap (λ p → p ∙ idp ∙' ! u)
+            (! (!-! u) ∙ ! (!-∙ (! u) idp)) ∙
+          ap (λ p → ! (! u ∙ idp) ∙ idp ∙' p)
+            (! (∙-unit-r (! u))) ∙ idp) ∙
+          ! (Ω-fmap-β (g , ! u ∙ idp) idp)) ∙ idp
+          =-=
+          snd (⊙Ω-fmap (g , ! u ∙ idp))
+      lemma idp = idp ◃∎
+
+  ap-comp-into-coher : {f g : Susp (de⊙ X) → de⊙ U} (H₀ : f ∼ g)
+    {gₚ : g (left unit) == f (left unit)} (H₁ : ! (H₀ (left unit)) ∙ idp == gₚ)
+    → ! (
+        (hmpty-nat-∙'-r H₀ (glue (pt X) ∙ ! (glue (pt X))) ∙
+        ap (λ p → p ∙ ap g (glue (pt X) ∙ ! (glue (pt X))) ∙' ! (H₀ (left unit)))
+          (! (!-! (H₀ (left unit))) ∙ ! (!-∙ (! (H₀ (left unit))) idp)) ∙
+        ap (λ p → ! (! (H₀ (left unit)) ∙ idp) ∙ ap g (glue (pt X) ∙ ! (glue (pt X))) ∙' p)
+          (! (∙-unit-r (! (H₀ (left unit))))) ∙
+        ∙-∙'-= (ap g (glue (pt X) ∙ ! (glue (pt X)))) H₁) ∙
+        ! (Ω-fmap-β (g , gₚ) (glue (pt X) ∙ ! (glue (pt X))))) ∙
+      ap (ap f) (!-inv-r (glue (pt X))) ∙ idp
+      =-=
+      ap (Ω-fmap (g , gₚ)) (!-inv-r (glue (pt X))) ∙ snd (⊙Ω-fmap (g , gₚ))
+  ap-comp-into-coher H₀ idp = ap-comp-into-coher-aux H₀ (glue (pt X))
+
+  ap-comp-into : {f₁ f₂ : ⊙Susp X ⊙→ U} (H : f₁ ⊙-comp f₂) → into f₁ ⊙-comp into f₂
+  fst (ap-comp-into {f₁ = (f , idp)} {f₂} H) x =
+    (hmpty-nat-∙'-r (fst H) (glue x ∙ ! (glue (pt X))) ∙
+      ap (λ p → p ∙ ap (λ z → fst f₂ z) (glue x ∙ ! (glue (pt X))) ∙' ! (fst H (left unit)))
+        (! (!-! (fst H (left unit))) ∙ ! (!-∙ (! (fst H (left unit))) idp)) ∙
+      ap (λ p → (! (! (fst H (left unit)) ∙ idp)) ∙ ap (fst f₂) (glue x ∙ ! (glue (pt X))) ∙' p)
+        (! (∙-unit-r (! (fst H (left unit))))) ∙
+      ∙-∙'-= (ap (fst f₂) (glue x ∙ ! (glue (pt X)))) (↯ (snd H))) ∙
+    ! (Ω-fmap-β f₂ (glue x ∙ ! (glue (pt X)))) 
+  snd (ap-comp-into {f₁ = (f , idp)} {f₂} H) = ap-comp-into-coher (fst H) (↯ (snd H))
+
+  {-
+     This definition of ap agrees with the standard ap on the id homotopy,
+     hence on all homotopies by the SIP.
+  -}
+
+  ap-comp-into-id : (f* : ⊙Susp X ⊙→ U) → ap-comp-into (⊙∼-id f*) ⊙→∼ ⊙∼-id (into f*)
+  fst (ap-comp-into-id (f , idp)) x = 
+    ∙-unit-r (hmpty-nat-∙'-r (λ x₁ → idp) (glue x ∙ ! (glue (pt X))) ∙ idp) ∙
+    ∙-unit-r (hmpty-nat-∙'-r (λ x₁ → idp) (glue x ∙ ! (glue (pt X)))) ∙
+    hmpty-nat-∙'-r-idp (glue x ∙ ! (glue (pt X)))
+  snd (ap-comp-into-id (f , idp)) = =ₛ-in (lemma (glue (pt X)))
+    where
+      lemma : {x : Susp (de⊙ X)} (v : x == right unit) →
+        ap (λ p → ! p ∙ ap (ap f) (!-inv-r v) ∙ idp)
+        (∙-unit-r (hmpty-nat-∙'-r (λ x₁ → idp) (v ∙ ! v) ∙ idp) ∙
+        ∙-unit-r (hmpty-nat-∙'-r (λ x₁ → idp) (v ∙ ! v)) ∙
+        hmpty-nat-∙'-r-idp (v ∙ ! v)) ∙ idp
+        ==
+        ↯ (ap-comp-into-coher-aux (λ x → idp) v)
+      lemma idp = idp
+      
+{-
+  an explicit component-based homotopy witnessing the
+  naturality of into in its first argument
+-}
+
+module _ {i i' j} {X : Ptd i} {Y : Ptd i'} {U : Ptd j} where 
+
+  module _ (r₀ : Susp (de⊙ Y) → de⊙ U) (h₀ : de⊙ X → de⊙ Y) where
+
+    nat-dom-aux-r : {v : Susp (de⊙ Y)} (τ : left unit == v)
+      →
+      ! (ap-∙ r₀ τ (! τ) ∙
+        (ap-!-inv r₀ τ ∙ ! (cmp-inv-r (glue (pt X)))) ∙
+        ! (ap (λ p → p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X))))
+        (ap-∘ r₀ (Susp-fmap h₀) (glue (pt X)))) ∙
+        ! (ap-∙ (r₀ ∘ Susp-fmap h₀) (glue (pt X)) (! (glue (pt X))))) ∙
+      ap (ap r₀) (!-inv-r τ) ∙ idp
+      ==
+      ap (ap (r₀ ∘ Susp-fmap h₀)) (!-inv-r (glue (pt X))) ∙ idp
+    nat-dom-aux-r idp = ap-!-∘-∙-rid-coher r₀ (Susp-fmap h₀) (glue (pt X))
+
+    nat-dom-aux-l2 : {v : Susp-fmap h₀ (left unit) == Susp-fmap h₀ (right unit)}
+      (τ : ap (Susp-fmap h₀) (glue (pt X)) == v)
+      →
+      ! (ap (_∙_ (ap r₀ v)) (ap (λ p → ap r₀ (! p)) τ)) ∙
+      ! (ap (_∙_ (ap r₀ v)) (ap-∘ r₀ (Susp-fmap h₀) (! (glue (pt X))) ∙
+        ap (ap r₀) (ap-! (Susp-fmap h₀) (glue (pt X))))) ∙
+      ! (ap (λ p → ap r₀ p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) τ)
+      ==
+      ap-!-inv r₀ v ∙ ! (cmp-inv-r (glue (pt X)))
+    nat-dom-aux-l2 idp = ap-!-∘-rid-coher r₀ (Susp-fmap h₀) (glue (pt X))
+    
+    nat-dom-aux-l : 
+      ! (ap (_∙_ (ap r₀ (glue (h₀ (pt X)))))
+        (ap (λ p → ap r₀ (! p))
+        (SuspFmap.merid-β h₀ (pt X)))) ∙
+      ! (ap (_∙_ (ap r₀ (glue (h₀ (pt X)))))
+        (ap-∘ r₀ (Susp-fmap h₀) (! (glue (pt X))) ∙
+        ap (ap r₀) (ap-! (Susp-fmap h₀) (glue (pt X))))) ∙
+      ! (ap (λ p → ap r₀ p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X))))
+        (SuspFmap.merid-β h₀ (pt X)))
+      ==
+      ap-!-inv r₀ ((merid ∘ h₀) (pt X)) ∙ ! (cmp-inv-r {f = Susp-fmap h₀} {g = r₀} (glue (pt X))) 
+    nat-dom-aux-l = nat-dom-aux-l2 (SuspFmap.merid-β h₀ (pt X)) 
+
+  nat-dom : (h : X ⊙→ Y) (r : ⊙Susp Y ⊙→ U)
+    → (into Y U) r ⊙∘ h ⊙-comp (into X U) (r ⊙∘ ⊙Susp-fmap h)
+  fst (nat-dom (h₀ , idp) (r₀ , idp)) x = ↯ (
+    ap-∙ r₀ (glue (h₀ x)) (! (glue (pt Y))) ◃∙
+    ! (ap (λ p → ap r₀ (glue (h₀ x)) ∙ p) (ap (λ p → ap r₀ (! p)) (SuspFmap.merid-β h₀ (pt X)))) ◃∙
+    ! (ap (λ p → ap r₀ (glue (h₀ x)) ∙ p) (ap-∘ r₀ (Susp-fmap h₀) (! (glue (pt X))) ∙
+      ap (ap r₀) (ap-! (Susp-fmap h₀) (glue (pt X))))) ◃∙
+    ! (ap (λ p → ap r₀ p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (SuspFmap.merid-β h₀ x)) ◃∙
+    ! ((ap (λ p → p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (ap-∘ r₀ (Susp-fmap h₀) (glue x)))) ◃∙
+    ! (ap-∙ (r₀ ∘ Susp-fmap h₀) (glue x) (! (glue (pt X)))) ◃∎
+    )
+  snd (nat-dom (h₀ , idp) (r₀ , idp)) =
+    ap (λ p → ! (ap-∙ r₀ (glue (h₀ (pt X))) (! (glue (h₀ (pt X)))) ∙ p) ∙
+      ap (ap r₀) (!-inv-r (glue (h₀ (pt X)))) ∙ idp)
+      (assoc-4-∙
+        (! (ap (_∙_ (ap r₀ (glue (h₀ (pt X))))) (ap (λ p → ap r₀ (! p)) (SuspFmap.merid-β h₀ (pt X)))))
+        (! (ap (_∙_ (ap r₀ (glue (h₀ (pt X))))) (ap-∘ r₀ (Susp-fmap h₀) (! (glue (pt X))) ∙
+          ap (ap r₀) (ap-! (Susp-fmap h₀) (glue (pt X))))))
+        (! (ap (λ p → ap r₀ p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (SuspFmap.merid-β h₀ (pt X))))
+        (! (ap (λ p → p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (ap-∘ r₀ (Susp-fmap h₀) (glue (pt X)))))
+        (! (ap-∙ (r₀ ∘ Susp-fmap h₀) (glue (pt X)) (! (glue (pt X)))))) ◃∙
+    ap (λ p → ! (ap-∙ r₀ (glue (h₀ (pt X))) (! (glue (h₀ (pt X)))) ∙ p ∙
+      ! (ap (λ p → p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (ap-∘ r₀ (Susp-fmap h₀) (glue (pt X)))) ∙
+      ! (ap-∙ (r₀ ∘ Susp-fmap h₀) (glue (pt X)) (! (glue (pt X))))) ∙
+        ap (ap r₀) (!-inv-r (glue (h₀ (pt X)))) ∙ idp) (nat-dom-aux-l r₀ h₀) ◃∙
+    nat-dom-aux-r r₀ h₀ ((glue (h₀ (pt X)))) ◃∎
+
+{- the nat-dom proof makes Susp a 2-coherent left adjoint to Loop -}
+
+-- an ad-hoc data structure for a messy computation required by our 2-coherence proof
+
+module _ {i j k l ℓ} {A : Type i} {B : Type j} {C : Type k} {D : Type l} {E : Type ℓ}
+  (m : A → D) (n : B → A) (s : C → A) (r : E → C) where
+
+  record sev_step_red_inp {x₁ x₂ : D} {x₃ x₄ : A} {x₅ x₆ x₇ : B} {x₈ x₁₃ : C}
+    {x₉ x₁₀ x₁₁ x₁₂ : E} (q₁ : x₁ == m x₃) (q₂ : x₄ == n x₅) (q₃ : x₅ == x₆)
+    (q₄ : x₆ == x₇) {b : B} (q₅ : x₇ == b) (ϕ : n b  == s x₈) (q₆ : x₈ == r x₉)
+    (q₇ : x₉ == x₁₀) (q₈ : x₁₀ == x₁₁) (q₉ : x₁₁ == x₁₂) (q₁₀ : r x₁₂ == x₁₃)
+    (q₁₁ : s x₁₃ == x₃) (q₁₂ : m x₄ == x₂) (τ : x₁ == x₂)
+    {d₀ d₁ d₂ d₃ d₄ d₅ d₆ d₇ : D}
+    (μ₁ : d₀ == d₁) (μ₂ : d₃ == d₄) (μ₃ : d₀ == d₆)
+    (p₁ : d₁ == d₂) (p₂ : d₂ == d₃) (p₃ : d₄ == d₅)
+    (p₄ : d₅ == x₁) (p₅ : d₆ == d₇) (p₆ : d₇ == x₂)
+    {R₁ : d₃ == m (s (r x₁₁))} {R₂ : d₃ == m (n x₇)} {R₃ : d₀ == m (n x₇)}
+    {R₄ : d₀ == m (n x₆)} {R₅ : m (n x₆) == d₇}
+      : Type (lmax i (lmax j (lmax k l))) where
+    constructor sev_step
+    field
+      red1 : τ == ((q₁ ∙ ! (ap m (q₂ ∙ ap n (q₃ ∙ q₄ ∙ q₅) ∙ ϕ ∙
+        ap s (q₆ ∙ ap r (q₇ ∙ q₈ ∙ q₉) ∙ q₁₀) ∙ q₁₁)) ∙ q₁₂) ∙ idp) ∙ idp
+      red2 : μ₂ ∙ p₃ ∙ p₄ ∙ q₁ ∙ ! (ap m (ap s (ap r q₉ ∙ q₁₀) ∙ q₁₁)) == R₁
+      red3 : R₁ ∙ ! (ap m (ap n q₅ ∙ ϕ ∙ ap s (q₆ ∙ ap r (q₇ ∙ q₈)))) == R₂
+      red4 : μ₁ ∙ p₁ ∙ p₂ ∙ R₂ == R₃
+      red5 : R₃ ∙ ! (ap m (ap n q₄)) == R₄
+      red6 : ! (ap m (q₂ ∙ ap n q₃)) ∙ q₁₂ ∙ ! p₆ == R₅
+      red7 : R₄ ∙ R₅ ∙ ! p₅ ∙ ! μ₃ == idp
+  open sev_step_red_inp public
+
+module _ {i j k l ℓ} {A : Type i} {B : Type j} {C : Type k} {D : Type l} {E : Type ℓ}
+  {m : A → D} {n : B → A} {s : C → A} {r : E → C} where
+
+  sev_step_reduce : {x₁ x₂ : D} {x₃ x₄ : A} {x₅ x₆ x₇ : B} {x₈ x₁₃ : C}
+    {x₉ x₁₀ x₁₁ x₁₂ : E} {q₁ : x₁ == m x₃} {q₂ : x₄ == n x₅} {q₃ : x₅ == x₆}
+    {q₄ : x₆ == x₇} {b : B} {q₅ : x₇ == b} {ϕ : n b  == s x₈} {q₆ : x₈ == r x₉}
+    {q₇ : x₉ == x₁₀} {q₈ : x₁₀ == x₁₁} {q₉ : x₁₁ == x₁₂} {q₁₀ : r x₁₂ == x₁₃}
+    {q₁₁ : s x₁₃ == x₃} {q₁₂ : m x₄ == x₂} {τ : x₁ == x₂}
+    {d₀ d₁ d₂ d₃ d₄ d₅ d₆ d₇ : D}
+    {μ₁ : d₀ == d₁} {μ₂ : d₃ == d₄} {μ₃ : d₀ == d₆}
+    {p₁ : d₁ == d₂} {p₂ : d₂ == d₃} {p₃ : d₄ == d₅}
+    {p₄ : d₅ == x₁} {p₅ : d₆ == d₇} {p₆ : d₇ == x₂}
+    {R₁ : d₃ == m (s (r x₁₁))} {R₂ : d₃ == m (n x₇)} {R₃ : d₀ == m (n x₇)}
+    {R₄ : d₀ == m (n x₆)} {R₅ : m (n x₆) == d₇}
+    → sev_step_red_inp m n s r q₁ q₂ q₃ q₄ q₅ ϕ
+      q₆ q₇ q₈ q₉ q₁₀ q₁₁ q₁₂ τ μ₁ μ₂ μ₃
+      p₁ p₂ p₃ p₄ p₅ p₆ {R₁} {R₂} {R₃} {R₄} {R₅}
+    → (μ₁ ∙ p₁ ∙ p₂) ∙ (μ₂ ∙ p₃ ∙ p₄) ∙ τ ∙ ! (μ₃ ∙ p₅ ∙ p₆) == idp
+  sev_step_reduce {q₁ = idp} {idp} {idp} {idp} {q₅ = idp}
+    {ϕ} {idp} {idp} {idp} {idp} {idp} {idp} {idp} {μ₁ = idp}
+    {idp} {idp} {idp} {idp} {idp} {idp} {idp} {p₆}
+    (sev_step idp idp idp idp idp idp red7) =
+      ap (λ p → p ∙ ! p₆) (∙-unit-r ((! (ap m (ϕ ∙ idp)) ∙ idp) ∙ idp) ∙ ∙-unit-r (! (ap m (ϕ ∙ idp)) ∙ idp)) ∙
+      ap (λ p → (! (ap m (ϕ ∙ idp)) ∙ idp) ∙ p) (! (∙-unit-r (! p₆))) ∙
+      red7
+
+module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : Ptd i₄} where 
+
+  -- unfolded version of naturality square for Susp-fmap-∘
+
+  module _ (f₂ : de⊙ Z → de⊙ X) (f₃ : de⊙ W → de⊙ Z) (f₁ : Susp (de⊙ X) → de⊙ Y)
+    (x : de⊙ W) where 
+
+    β-free1 : {x : Susp (de⊙ Z)} {ω₁ : left unit == right unit}
+      (ω₂ : x == right unit) (ω₃ : left unit == right unit)
+      (ω₄ : ap (Susp-fmap f₃) ω₃ == ω₁) →
+      ap (f₁ ∘ Susp-fmap f₂) (ω₁ ∙ ! ω₂)
+      ==
+      ap f₁ (ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ ∙
+        ! (ap (Susp-fmap f₂) ω₂))
+    β-free1 {ω₁ = ω₁} ω₂ ω₃ ω₄ =
+      ap-∘ f₁ (Susp-fmap f₂) (ω₁ ∙ ! ω₂) ∙
+      ap (ap f₁) (ap-∙ (Susp-fmap f₂) ω₁ (! ω₂)) ∙
+      ! (ap (ap f₁) (ap (λ p → p ∙ ap (Susp-fmap f₂) (! ω₂))
+        (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₃ ∙
+        ap (ap (Susp-fmap f₂)) ω₄))) ∙
+      ap (ap f₁) (ap (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ ∙ p)
+        (ap-! (Susp-fmap f₂) ω₂))
+
+    β-red1-aux2 : {w : Susp (de⊙ W)} (ω₆ : left unit == w)
+      {𝕗 : ap f₁ (! (SuspMapEq (Susp-fmap (f₂ ∘ f₃))
+        (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (Susp-fmap-∘ f₂ f₃) w)) ∙
+      ap f₁ (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
+        idp idp (Susp-fmap-∘ f₂ f₃) w ∙
+        ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆))
+      == ap f₁ (ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆))}
+      (𝕣 : 𝕗 == ap-!-∙-ap f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆)
+        (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
+        idp idp (Susp-fmap-∘ f₂ f₃) w)) →
+      (! (ap (λ q → q) (ap-∘ (f₁ ∘ Susp-fmap f₂) (Susp-fmap f₃) (! ω₆) ∙
+        ap (ap (f₁ ∘ Susp-fmap f₂)) (ap-! (Susp-fmap f₃) ω₆))) ∙ idp) ∙
+      ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃))
+        (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
+        idp idp (Susp-fmap-∘ f₂ f₃)) (! ω₆) ∙
+      𝕗 ∙ 
+      ! (ap (ap f₁) (ap (λ q → q) (ap ! (! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₆)) ∙
+        !-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₆) ∙ idp))
+      ==
+      ap-∘ f₁ (Susp-fmap f₂) (! (ap (Susp-fmap f₃) ω₆)) ∙
+      ap (ap f₁) (ap (λ q → q) (ap-! (Susp-fmap f₂) (ap (Susp-fmap f₃) ω₆)))
+    β-red1-aux2 idp idp = idp
+
+    β-red1-aux : {w : Susp (de⊙ W)} (ω₃ ω₆ : left unit == w) →
+      ap-∙ (f₁ ∘ Susp-fmap f₂) (ap (Susp-fmap f₃) ω₃)
+        (! (ap (Susp-fmap f₃) ω₆)) ∙
+      (! (ap (_∙_ (ap (f₁ ∘ Susp-fmap f₂) (ap (Susp-fmap f₃) ω₃)))
+        (ap-∘ (f₁ ∘ Susp-fmap f₂) (Susp-fmap f₃) (! ω₆) ∙
+        ap (ap (f₁ ∘ Susp-fmap f₂)) (ap-! (Susp-fmap f₃) ω₆))) ∙
+      ! (ap (λ p → p ∙ ap (f₁ ∘ Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆))
+        (ap-∘ (f₁ ∘ Susp-fmap f₂) (Susp-fmap f₃) ω₃)) ∙
+      ! (ap-∙ (f₁ ∘ Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ (! ω₆))) ∙
+      ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃))
+        (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
+        idp idp (Susp-fmap-∘ f₂ f₃)) (ω₃ ∙ ! ω₆) ∙
+      ! (ap (ap f₁) (ap (_∙_ (ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃))
+        (ap ! (! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₆)) ∙
+        !-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₆) ∙
+        ap (λ p → p) (! (ap-∙ (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ (! ω₆)))))
+      ==
+      ap-∘ f₁ (Susp-fmap f₂) ((ap (Susp-fmap f₃) ω₃) ∙
+        ! (ap (Susp-fmap f₃) ω₆)) ∙
+      ap (ap f₁) (ap-∙ (Susp-fmap f₂) (ap (Susp-fmap f₃) ω₃)
+        (! (ap (Susp-fmap f₃) ω₆))) ∙
+      ! (ap (ap f₁) (ap (λ p → p ∙ ap (Susp-fmap f₂) (! (ap (Susp-fmap f₃) ω₆)))
+        (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₃ ∙ idp))) ∙
+      ap (ap f₁) (ap (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ ∙ p)
+        (ap-! (Susp-fmap f₂) (ap (Susp-fmap f₃) ω₆)))
+    β-red1-aux idp ω₆ = β-red1-aux2 ω₆ idp
+ 
+    β-red1 : {ω₁ ω₂ : left unit == right unit}
+      (ω₃ : left unit == right unit) (ω₄ : ap (Susp-fmap f₃) ω₃ == ω₁)
+      (ω₆ : left unit == right unit) (ω₅ : ap (Susp-fmap f₃) ω₆ == ω₂) → 
+      ap-∙ (f₁ ∘ Susp-fmap f₂) ω₁ (! ω₂) ∙
+      ! (ap (_∙_ (ap (f₁ ∘ Susp-fmap f₂) ω₁))
+        (ap (λ p → ap (f₁ ∘ Susp-fmap f₂) (! p)) ω₅)) ∙
+      (! (ap (_∙_ (ap (f₁ ∘ Susp-fmap f₂) ω₁))
+        (ap-∘ (f₁ ∘ Susp-fmap f₂) (Susp-fmap f₃) (! ω₆) ∙
+        ap (ap (f₁ ∘ Susp-fmap f₂)) (ap-! (Susp-fmap f₃) ω₆))) ∙
+      ! (ap (λ p → ap (f₁ ∘ Susp-fmap f₂) p ∙ ap ((f₁ ∘ Susp-fmap f₂) ∘ Susp-fmap f₃)
+        (! ω₆)) ω₄) ∙
+      ! (ap (λ p → p ∙ ap (f₁ ∘ Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆))
+        (ap-∘ (f₁ ∘ Susp-fmap f₂) (Susp-fmap f₃) ω₃)) ∙
+      ! (ap-∙ (f₁ ∘ Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ (! ω₆))) ∙
+      ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃))
+        (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
+        idp idp (Susp-fmap-∘ f₂ f₃)) (ω₃ ∙ ! ω₆) ∙
+      ! (ap (ap f₁) (ap (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ ∙ p)
+          (ap ! (! (ap (ap (Susp-fmap f₂)) ω₅) ∙
+          ! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₆)) ∙
+          !-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₆) ∙
+        ap (λ p → p) (! (ap-∙ (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃
+          (! ω₆)))))
+      == β-free1 ω₂ ω₃ ω₄
+    β-red1 ω₃ idp ω₆ idp = β-red1-aux ω₃ ω₆
+
+    β-free2 : {x₁ x₂ x₃ : Susp (de⊙ Z)} (ω₁ : x₂ == x₃)
+      (ω₂ : x₁ == x₃) {ω₇ : Susp-fmap f₂ x₃ == Susp-fmap f₂ x₁}
+      (ω₈ : ω₇ == ! (ap (Susp-fmap f₂) ω₂)) → 
+      ap (f₁ ∘ Susp-fmap f₂) (ω₁ ∙ ! ω₂)
+      ==
+      ap f₁ (ap (Susp-fmap f₂) ω₁ ∙ ω₇)
+    β-free2 ω₁ ω₂ ω₈ =
+      ap-∘ f₁ (Susp-fmap f₂) (ω₁ ∙ ! ω₂) ∙
+      ap (ap f₁) (ap-∙ (Susp-fmap f₂) ω₁ (! ω₂)) ∙
+      ap (ap f₁) (ap (λ p → ap (Susp-fmap f₂) ω₁ ∙ p) (ap-! (Susp-fmap f₂) ω₂)) ∙
+      ap (ap f₁) (ap (λ p → ap (Susp-fmap f₂) ω₁ ∙ p) (! ω₈))
+
+    β-red2-aux2 : {x₁ x₂ : Susp (de⊙ Z)} (ω₂ : x₁ == x₂)
+      {c : Susp-fmap f₂ x₂ == Susp-fmap f₂ x₁}
+      (↑ω₈ : c == ! (ap (Susp-fmap f₂) ω₂)) →
+      (ap-∘ f₁ (Susp-fmap f₂) (! ω₂) ∙
+        ap (ap f₁) (ap (λ q → q) (ap-! (Susp-fmap f₂) ω₂))) ∙
+      ! (ap (ap f₁) (ap (λ q → q) ↑ω₈))
+      ==
+      β-free2 idp ω₂ ↑ω₈
+    β-red2-aux2 idp idp = idp
+
+    β-red2-aux : {w : Susp (de⊙ W)} (ω₃ : w == right unit)
+      (ω₂ : left unit == right unit)
+      (ω₆ : left unit == right unit)
+      (ω₈¹ : ap (Susp-fmap (f₂ ∘ f₃)) ω₆ == ap (Susp-fmap f₂) ω₂) → 
+      (ap-∘ f₁ (Susp-fmap f₂) (ap (Susp-fmap f₃) ω₃ ∙ ! ω₂) ∙
+      ap (ap f₁) (ap-∙ (Susp-fmap f₂) (ap (Susp-fmap f₃) ω₃) (! ω₂)) ∙
+      ! (ap (ap f₁) (ap (λ p → p ∙ ap (Susp-fmap f₂) (! ω₂))
+        (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₃ ∙ idp))) ∙
+      ap (ap f₁) (ap (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ ∙ p)
+        (ap-! (Susp-fmap f₂) ω₂))) ∙
+      ! (ap (ap f₁) (ap (λ p → p ∙
+        ap (Susp-fmap (f₂ ∘ f₃)) (! ω₆))
+        (! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₃)) ∙
+        ap (_∙_ (ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃))
+        (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙ ap ! (ω₈¹ ∙ idp))))
+      ==
+      β-free2 (ap (Susp-fmap f₃) ω₃) ω₂
+        (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙ ap ! (ω₈¹ ∙ idp))
+    β-red2-aux idp ω₂ ω₆ ω₈¹ =
+      β-red2-aux2 ω₂ (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙ ap ! (ω₈¹ ∙ idp))
+
+    β-red2 : (ω₂ : left unit == right unit)
+      (ω₃ : left unit == right unit)
+      (ω₆ : left unit == right unit)
+      {w : left unit == right unit}
+      (ω₈² : ap (Susp-fmap f₂) ω₂ == w)
+      (ω₈¹ : ap (Susp-fmap (f₂ ∘ f₃)) ω₆ == w)
+      {e : Susp-fmap f₃ (left unit) == Susp-fmap f₃ (right unit)}
+      (ω₉ : ap (Susp-fmap f₃) ω₃ == e) →
+      β-free1 ω₂ ω₃ ω₉ ∙
+      ! (ap (ap f₁) (ap (λ p → p ∙ ap (Susp-fmap (f₂ ∘ f₃)) (! ω₆))
+        (! (ap (ap (Susp-fmap f₂)) ω₉) ∙
+        ! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₃)) ∙
+        ap (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ ∙ p)
+        (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙ ap ! (ω₈¹ ∙ ! ω₈²))))
+      ==
+      β-free2 e ω₂ ((ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙ ap ! (ω₈¹ ∙ ! ω₈²)))
+    β-red2 ω₂ ω₃ ω₆ idp ω₈¹ idp = β-red2-aux ω₃ ω₂ ω₆ ω₈¹
+
+    β-free3 : {y : Susp (de⊙ Z)} (ω₁ : y == right unit)
+      {x : Susp (de⊙ W)} (ω₆ : x == right unit)
+      {ω₁₁ : Susp-fmap (f₂ ∘ f₃) x == right unit}
+      (ω₈¹ : ap (Susp-fmap (f₂ ∘ f₃)) ω₆ == ω₁₁)
+      {ω₁₀ : Susp-fmap f₂ y == right unit}
+      (ω₁₂ : ap (Susp-fmap f₂) ω₁ == ω₁₀) → 
+      ap f₁ (ω₁₀ ∙ ! ω₁₁)
+      ==
+      ap f₁ (ap (Susp-fmap f₂) ω₁ ∙
+        ap (Susp-fmap (f₂ ∘ f₃)) (! ω₆))
+    β-free3 ω₁ ω₆ {ω₁₁} ω₈¹ {ω₁₀} ω₁₂ =
+      ap (λ p → ap f₁ (p ∙ ! ω₁₁)) (! ω₁₂) ∙
+      ap (λ p → ap f₁ (ap (Susp-fmap f₂) ω₁ ∙ ! p)) (! ω₈¹) ∙
+      ap (λ p → ap f₁ (ap (Susp-fmap f₂) ω₁ ∙ p))
+        (!-ap (Susp-fmap (f₂ ∘ f₃)) ω₆)  
+
+    β-red3 : {y : Susp (de⊙ Z)} (ω₁ : y == right unit)
+      (ω₂ : left unit == right unit)
+      (ω₆ : left unit == right unit)
+      {ω₁₁ : left unit == right unit}
+      (ω₈² : ap (Susp-fmap f₂) ω₂ == ω₁₁)
+      (ω₈¹ : ap (Susp-fmap (f₂ ∘ f₃)) ω₆ == ω₁₁)
+      {ω₁₀ : Susp-fmap f₂ y == right unit}
+      (ω₁₂ : ap (Susp-fmap f₂) ω₁ == ω₁₀) →
+      ap-∙ f₁ ω₁₀ (! ω₁₁) ∙
+      ! (ap (_∙_ (ap f₁ ω₁₀))
+        (ap (λ p → ap f₁ (! p)) ω₈²)) ∙
+      (! (ap (_∙_ (ap f₁ ω₁₀))
+         (ap-∘ f₁ (Susp-fmap f₂) (! ω₂) ∙
+         ap (ap f₁) (ap-! (Susp-fmap f₂) ω₂))) ∙
+      ! (ap (λ p → ap f₁ p ∙ ap (f₁ ∘ Susp-fmap f₂) (! ω₂)) ω₁₂) ∙
+      ! (ap (λ p → p ∙ ap (f₁ ∘ Susp-fmap f₂) (! ω₂))
+        (ap-∘ f₁ (Susp-fmap f₂) ω₁)) ∙
+      ! (ap-∙ (f₁ ∘ Susp-fmap f₂) ω₁ (! ω₂))) ∙
+      β-free2 ω₁ ω₂ (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙
+        ap ! (ω₈¹ ∙ ! ω₈²))
+      ==
+      ap (λ p → ap f₁ (p ∙ ! ω₁₁)) (! ω₁₂) ∙
+      ap (λ p → ap f₁ (ap (Susp-fmap f₂) ω₁ ∙ ! p)) (! ω₈¹) ∙
+      ap (λ p → ap f₁ (ap (Susp-fmap f₂) ω₁ ∙ p))
+        (!-ap (Susp-fmap (f₂ ∘ f₃)) ω₆)
+    β-red3 idp ω₂ ω₆ idp ω₈¹ idp = 
+      ap-∘2-ap-! f₁ (Susp-fmap f₂) ω₂
+        (ap (ap f₁) (ap (λ p → p) (! (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙
+        ap ! (ω₈¹ ∙ idp))))) ∙
+      ap3-!-ap-!-rid (Susp-fmap (f₂ ∘ f₃)) f₁ ω₆ ω₈¹
+
+    β-red4 : {y : Susp (de⊙ Z)} (ω₁ : y == right unit)
+      {w : Susp (de⊙ W)} (ω₆ : w == right unit)
+      {ω₁₁ : Susp-fmap (f₂ ∘ f₃) w == right unit}
+      (ω₈¹ : ap (Susp-fmap (f₂ ∘ f₃)) ω₆ == ω₁₁)
+      {ω₁₀ : Susp-fmap f₂ y == right unit}
+      (ω₁₂ : ap (Susp-fmap f₂) ω₁ == ω₁₀) → 
+      (ap (λ p → ap f₁ (p ∙ ! ω₁₁)) (! ω₁₂) ∙
+      ap (λ p → ap f₁ (ap (Susp-fmap f₂) ω₁ ∙ ! p))
+        (! ω₈¹) ∙
+      ap (λ p → ap f₁ (ap (Susp-fmap f₂) ω₁ ∙ p))
+        (!-ap (Susp-fmap (f₂ ∘ f₃)) ω₆)) ∙
+      ! (ap (ap f₁) (ap (λ p → p ∙ ap (Susp-fmap (f₂ ∘ f₃))
+        (! ω₆)) (! ω₁₂)))
+      ==
+      ap (λ p → ap f₁ (ω₁₀ ∙ p))
+        (! (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙ ap ! ω₈¹))
+    β-red4 idp idp idp idp = idp
+
+    β-red5 : {w : Susp (de⊙ W)} (ω₆ : w == right unit)
+      (ω₃ : left unit == right unit)
+      {ω₁₀ : left unit == right unit}
+      (ω₁₃ : ap (Susp-fmap (f₂ ∘ f₃)) ω₃ == ω₁₀) → 
+      ! (ap (ap f₁) (ap-∙ (Susp-fmap (f₂ ∘ f₃)) ω₃
+        (! ω₆) ∙ ap (λ p → p ∙ ap (Susp-fmap (f₂ ∘ f₃))
+        (! ω₆)) ω₁₃)) ∙
+      ! (ap (λ q → q) (ap-∘ f₁ (Susp-fmap (f₂ ∘ f₃))
+        (ω₃ ∙ ! ω₆))) ∙
+      ! (! (ap (_∙_ (ap f₁ ω₁₀))
+          (ap-∘ f₁ (Susp-fmap (f₂ ∘ f₃)) (! ω₆) ∙
+          ap (ap f₁) (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆))) ∙
+        ! (ap (λ p → ap f₁ p ∙ ap (f₁ ∘ Susp-fmap (f₂ ∘ f₃))
+          (! ω₆)) ω₁₃) ∙
+        ! (ap (λ p → p ∙ ap (f₁ ∘ Susp-fmap (f₂ ∘ f₃)) (! ω₆))
+          (ap-∘ f₁ (Susp-fmap (f₂ ∘ f₃)) ω₃)) ∙
+        ! (ap-∙ (f₁ ∘ Susp-fmap (f₂ ∘ f₃)) ω₃ (! ω₆)))
+      ==
+      ap-∙ f₁ ω₁₀ (ap (Susp-fmap (f₂ ∘ f₃)) (! ω₆)) ∙
+      ap (λ p → ap f₁ ω₁₀ ∙ ap f₁ p)
+        (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆)
+    β-red5 idp ω₃ idp = ap-∘2-ap-∙ f₁ (Susp-fmap (f₂ ∘ f₃)) ω₃
+
+    β-red6 : {x : Susp (de⊙ X)} (ω₁₀ : x == right unit)
+      {w : Susp (de⊙ W)} (ω₆ : w == right unit)
+      {ω₁₁ : Susp-fmap (f₂ ∘ f₃) w == right unit}
+      (ω₈¹ : ap (Susp-fmap (f₂ ∘ f₃)) ω₆ == ω₁₁) →
+      ap (λ p → ap f₁ (ω₁₀ ∙ p))
+        (! (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆ ∙
+        ap ! ω₈¹)) ∙
+      (ap-∙ f₁ ω₁₀ (ap (Susp-fmap (f₂ ∘ f₃)) (! ω₆)) ∙
+      ap (λ p → ap f₁ ω₁₀ ∙ ap f₁ p)
+        (ap-! (Susp-fmap (f₂ ∘ f₃)) ω₆)) ∙
+      ! (! (ap (_∙_ (ap f₁ ω₁₀))
+        (ap (λ p → ap f₁ (! p)) ω₈¹))) ∙
+      ! (ap-∙ f₁ ω₁₀ (! ω₁₁))
+      == idp
+    β-red6 idp idp idp = idp
+
+    Susp-fmap-∘-sq-rw : 
+      (hmpty-nat-∙'-r (λ z → ap f₁ (! (Susp-fmap-∘-∼ f₂ f₃ z)))
+        (merid x ∙ ! (merid (pt W))) ∙ idp) ∙ idp
+        ==
+      ((ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃))
+        (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
+        idp idp (Susp-fmap-∘ f₂ f₃)) (merid x ∙ ! (merid (pt W))) ∙
+      ! (ap (ap f₁) (
+        ap-∙ (Susp-fmap (f₂ ∘ f₃)) (merid x) (! (merid (pt W))) ∙
+        ap (λ p → p ∙ ap (Susp-fmap (f₂ ∘ f₃)) (! (merid (pt W))))
+          (SuspFmap.merid-β (f₂ ∘ f₃) x ∙ ! (SuspFmap.merid-β f₂ (f₃ x)) ∙
+          ! (ap (ap (Susp-fmap f₂)) (SuspFmap.merid-β f₃ x)) ∙
+          ! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) (merid x))) ∙
+        ap (_∙_ (ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (merid x)))
+          (ap-! (Susp-fmap (f₂ ∘ f₃)) (merid (pt W)) ∙
+          ap ! (SuspFmap.merid-β (f₂ ∘ f₃) (pt W) ∙
+            ! (SuspFmap.merid-β f₂ (f₃ (pt W))) ∙
+            ! (ap (ap (Susp-fmap f₂)) (SuspFmap.merid-β f₃ (pt W))) ∙
+            ! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) (merid (pt W)))) ∙
+          !-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (merid (pt W))) ∙
+        ap (λ p → p) (! (ap-∙ (Susp-fmap f₂ ∘ Susp-fmap f₃) (merid x)
+          (! (merid (pt W))))))) ∙
+      ! (ap (λ q → q) (ap-∘ f₁ (Susp-fmap (f₂ ∘ f₃))
+        (merid x ∙ ! (merid (pt W)))))) ∙
+      idp) ∙ idp
+    Susp-fmap-∘-sq-rw = ap (λ p → (p ∙ idp) ∙ idp) (SuspMapEq-β-∙-ap! (Susp-fmap (f₂ ∘ f₃))
+      (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (Susp-fmap-∘ f₂ f₃) f₁ x (pt W))
+
+    -- proof of 2-coherence
+
+    two_coher_Susp-∼ : sev_step_red_inp (ap f₁)
+      (λ p → p ∙ ap (Susp-fmap (f₂ ∘ f₃)) (! (merid (pt W))))
+      (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (merid x) ∙ p) !
+      (ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃))
+        (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
+        idp idp (Susp-fmap-∘ f₂ f₃)) (merid x ∙ ! (merid (pt W))))
+      (ap-∙ (Susp-fmap (f₂ ∘ f₃)) (merid x) (! (merid (pt W))))
+      (SuspFmap.merid-β (f₂ ∘ f₃) x)
+      (! (SuspFmap.merid-β f₂ (f₃ x)))
+      (! (ap (ap (Susp-fmap f₂)) (SuspFmap.merid-β f₃ x)) ∙
+        ! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) (merid x)))
+      idp (ap-! (Susp-fmap (f₂ ∘ f₃)) (merid (pt W)))
+      (SuspFmap.merid-β (f₂ ∘ f₃) (pt W))
+      (! (SuspFmap.merid-β f₂ (f₃ (pt W))))
+      (! (ap (ap (Susp-fmap f₂)) (SuspFmap.merid-β f₃ (pt W))) ∙
+        ! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) (merid (pt W))))
+      (!-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (merid (pt W)))
+      (ap (λ p → p) (! (ap-∙ (Susp-fmap f₂ ∘ Susp-fmap f₃) (merid x)
+        (! (merid (pt W))))))
+      (! (ap (λ q → q) (ap-∘ f₁ (Susp-fmap (f₂ ∘ f₃))
+        (merid x ∙ ! (merid (pt W))))))
+      ((hmpty-nat-∙'-r (λ z → ap f₁ (! (Susp-fmap-∘-∼ f₂ f₃ z)))
+        (merid x ∙ ! (merid (pt W))) ∙ idp) ∙ idp)
+      (ap-∙ f₁ (merid (f₂ (f₃ x))) (! (merid (f₂ (f₃ (pt W))))))
+      (ap-∙ (f₁ ∘ (Susp-fmap f₂)) (merid (f₃ x)) (! (merid (f₃ (pt W)))))
+      (ap-∙ f₁ (merid (f₂ (f₃ x))) (! (merid (f₂ (f₃ (pt W))))))
+      (! (ap (_∙_ (ap f₁ (merid (f₂ (f₃ x))))) (ap (λ p → ap f₁ (! p))
+        (SuspFmap.merid-β f₂ (f₃ (pt W))))))
+      (! (ap (_∙_ (ap f₁ (merid (f₂ (f₃ x)))))
+        (ap-∘ f₁ (Susp-fmap f₂) (! (merid (f₃ (pt W)))) ∙
+        ap (ap f₁) (ap-! (Susp-fmap f₂) (merid (f₃ (pt W)))))) ∙
+      ! (ap (λ p → ap f₁ p ∙ ap (f₁ ∘ Susp-fmap f₂) (! (merid (f₃ (pt W)))))
+        (SuspFmap.merid-β f₂ (f₃ x))) ∙
+      ! (ap (λ p → p ∙ ap (f₁ ∘ Susp-fmap f₂) (! (merid (f₃ (pt W)))))
+        (ap-∘ f₁ (Susp-fmap f₂) (merid (f₃ x)))) ∙
+      ! (ap-∙ (f₁ ∘ Susp-fmap f₂) (merid (f₃ x)) (! (merid (f₃ (pt W))))))
+      (! (ap (_∙_ (ap (f₁ ∘ (Susp-fmap f₂)) (merid (f₃ x))))
+        (ap (λ p → ap (f₁ ∘ (Susp-fmap f₂)) (! p))
+        (SuspFmap.merid-β f₃ (pt W)))))
+      (! (ap (_∙_ (ap (f₁ ∘ (Susp-fmap f₂)) (merid (f₃ x))))
+        (ap-∘ (f₁ ∘ (Susp-fmap f₂)) (Susp-fmap f₃) (! (merid (pt W))) ∙
+        ap (ap (f₁ ∘ (Susp-fmap f₂))) (ap-! (Susp-fmap f₃) (merid (pt W))))) ∙
+      ! (ap (λ p → ap (f₁ ∘ (Susp-fmap f₂)) p ∙
+        ap (f₁ ∘ (Susp-fmap f₂) ∘ Susp-fmap f₃) (! (merid (pt W))))
+        (SuspFmap.merid-β f₃ x)) ∙
+      ! (ap (λ p → p ∙ ap (f₁ ∘ (Susp-fmap f₂) ∘ Susp-fmap f₃)
+        (! (merid (pt W)))) (ap-∘ (f₁ ∘ (Susp-fmap f₂)) (Susp-fmap f₃)
+        (merid x))) ∙
+      ! (ap-∙ (f₁ ∘ (Susp-fmap f₂) ∘ Susp-fmap f₃)
+        (merid x) (! (merid (pt W)))))
+      (! (ap (_∙_ (ap f₁ (merid (f₂ (f₃ x))))) (ap (λ p → ap f₁ (! p))
+        (SuspFmap.merid-β (f₂ ∘ f₃) (pt W)))))
+      (! (ap (_∙_ (ap f₁ (merid (f₂ (f₃ x))))) (ap-∘ f₁ (Susp-fmap (f₂ ∘ f₃))
+        (! (merid (pt W))) ∙ ap (ap f₁)
+        (ap-! (Susp-fmap (f₂ ∘ f₃)) (merid (pt W))))) ∙
+      ! (ap (λ p → ap f₁ p ∙ ap (f₁ ∘ Susp-fmap (f₂ ∘ f₃))
+        (! (merid (pt W)))) (SuspFmap.merid-β (f₂ ∘ f₃) x)) ∙
+      ! (ap (λ p → p ∙ ap (f₁ ∘ Susp-fmap (f₂ ∘ f₃)) (! (merid (pt W))))
+        (ap-∘ f₁ (Susp-fmap (f₂ ∘ f₃)) (merid x))) ∙
+      ! (ap-∙ (f₁ ∘ Susp-fmap (f₂ ∘ f₃)) (merid x) (! (merid (pt W)))))
+    red1 two_coher_Susp-∼ = Susp-fmap-∘-sq-rw
+    red2 two_coher_Susp-∼ = 
+      β-red1 (merid x) (SuspFmap.merid-β f₃ x) (merid (pt W))
+        (SuspFmap.merid-β f₃ (pt W))
+    red3 two_coher_Susp-∼ = 
+      β-red2 (merid (f₃ (pt W))) (merid x) (merid (pt W))
+        (SuspFmap.merid-β f₂ (f₃ (pt W)))
+        (SuspFmap.merid-β (f₂ ∘ f₃) (pt W))
+        (SuspFmap.merid-β f₃ x)
+    red4 two_coher_Susp-∼ =
+      β-red3 (merid (f₃ x)) (merid (f₃ (pt W))) (merid (pt W))
+      (SuspFmap.merid-β f₂ (f₃ (pt W))) (SuspFmap.merid-β (f₂ ∘ f₃) (pt W))
+      (SuspFmap.merid-β f₂ (f₃ x))
+    red5 two_coher_Susp-∼ =
+      β-red4 (merid (f₃ x)) (merid (pt W))
+        (SuspFmap.merid-β (f₂ ∘ f₃) (pt W))
+        (SuspFmap.merid-β f₂ (f₃ x))
+    red6 two_coher_Susp-∼ =
+      β-red5 (merid (pt W)) (merid x) (SuspFmap.merid-β (f₂ ∘ f₃) x) 
+    red7 two_coher_Susp-∼ =
+      β-red6 (merid (f₂ (f₃ x))) (merid (pt W))
+        (SuspFmap.merid-β (f₂ ∘ f₃) (pt W))
+
+  {-
+    It suffices to prove that the underlying homotopies are equal
+    because loop spaces are coherently homogeneous.
+  -}
+  
+  two_coher_Susp : (h₁ : ⊙Susp X ⊙→ Y) (h₂ : Z ⊙→ X) (h₃ : W ⊙→ Z) →
+    !-⊙∼ (⊙∘-assoc-comp (into X Y h₁) h₂ h₃) ∙⊙∼
+    ⊙∘-pre h₃ (nat-dom h₂ h₁) ∙⊙∼
+    nat-dom h₃ (h₁ ⊙∘ ⊙Susp-fmap h₂) ∙⊙∼
+    ap-comp-into W Y (⊙∘-assoc-comp h₁ (⊙Susp-fmap h₂) (⊙Susp-fmap h₃) ∙⊙∼
+      ⊙∘-post h₁ (!-⊙∼ (Susp-fmap-∘-∼ (fst h₂) (fst h₃) , idp ◃∎))) ∙⊙∼
+    !-⊙∼ (nat-dom (h₂ ⊙∘ h₃) h₁)
+      ⊙→∼
+    ⊙∼-id ((into X Y h₁) ⊙∘ h₂ ⊙∘ h₃)
+  two_coher_Susp (f₁ , idp) (f₂ , idp) (f₃ , idp) =
+    ∼⊙Ωhomog∼ λ x → sev_step_reduce (two_coher_Susp-∼ f₂ f₃ f₁ x)
diff --git a/README.md b/README.md
index 929a68e..eda40b0 100644
--- a/README.md
+++ b/README.md
@@ -8,18 +8,24 @@
 - `HoTT-Agda/`
 
   A stripped down version of Andrew Swan's [HoTT-Agda](https://github.com/awswan/HoTT-Agda/tree/agda-2.6.1-compatible) branch,
-  with local changes for general lemmas we proved during the development.
+  with local changes for general lemmas we proved during the development. It also includes a proof of the 2-coherence of
+  the Suspension-Loop adjunction and some properties of homogeneous types (used for the proof of 2-coherence).
+
+  See `HoTT-Agda/README.md` for the license of the work inside this directory.
 
 - `Colimit-code/`
 
   Our formalization of our construction of an A-colimit.
+
   See `Colimit-code/README.md` for details and for the
   license of the work inside this directory.
 
 - `Pullback-stability/`
 
   Our formalization of pullback stability (or universality)
-  for all ordinary colimits. See `Pullback-stability/README.md`
+  for all ordinary colimits.
+
+  See `Pullback-stability/README.md`
   for details and for the license of the work inside this
   directory.