diff --git a/Colimit-code/Map-Nat/CosColimitPstCmp.agda b/Colimit-code/Map-Nat/CosColimitPstCmp.agda
index 827fe1f..6c3b9fd 100644
--- a/Colimit-code/Map-Nat/CosColimitPstCmp.agda
+++ b/Colimit-code/Map-Nat/CosColimitPstCmp.agda
@@ -14,9 +14,9 @@ module CosColimitPstCmp where
 
 module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} (h : B → C) (f : A → B) where 
 
-  ap-∘-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c} 
+  ap-∘-∙-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c} 
     → ap h (ap f p₁ ∙ p₂) ∙ s == ap (h ∘ f) p₁ ∙ ap h p₂ ∙ s
-  ap-∘-∙ idp p₂ = idp
+  ap-∘-∙-∙ idp p₂ = idp
 
   ap-∘-rid : {x y : A} (p : x == y) → ap h (ap f p) ∙ idp == ap (h ∘ f) p
   ap-∘-rid idp = idp
@@ -71,7 +71,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
           ap φ₁ (ap f p₁) ∙ idp) ∙
           ap (φ₁ ∘ f ∘ right ∘ cin j) p₂ ∙
           ap (φ₁ ∘ f) p₃ ∙ ap φ₁ p₄ ∙ p₅))
-          (ap-∘-∙ φ₁ f p₃ p₄)  ◃∙
+          (ap-∘-∙-∙ φ₁ f p₃ p₄)  ◃∙
         long-path-red p₂
           (ap (φ₁ ∘ f) p₃ ∙
           ap φ₁ p₄ ∙ p₅)
@@ -98,7 +98,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
           ap (λ p → ap φ₁ p ∙ φ₂ a) (ap-cp-revR f (right ∘ cin j) p₂
             p₁ ∙
           ap (λ p → p ∙ fₚ a) (ap (ap f) τ))) ◃∙
-      ap-∘-∙ φ₁ f σ (fₚ a) ◃∎
+      ap-∘-∙-∙ φ₁ f σ (fₚ a) ◃∎
       =ₛ
       (ap-cp-revR (φ₁ ∘ f) (right ∘ cin j)
         p₂ p₁ ∙
@@ -107,14 +107,14 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
     NatSq-1-Λ-red2 {i} {j} g a idp idp p₃ idp = =ₛ-in (lemma p₃ (fₚ a))
       where
         lemma : {z : P} (p : right (cin j (fst (F <#> g) (fun (F # i) a))) == z) (c : f z == fun T a)
-          → ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙ φ₁ f p c == idp
+          → ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙-∙ φ₁ f p c == idp
         lemma idp c = idp
 
 -- τ = (snd (comTri ColCoC g) a)
 
     CosColim-NatSq1 : CosCocEq F U (Map-to-Lim-map (PostComp ColCoC (f , fₚ))) (PostComp ColCoC (φ ∘* (f , fₚ)))
     W CosColim-NatSq1 = λ i x → idp
-    u CosColim-NatSq1 = λ i a → ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a)  
+    u CosColim-NatSq1 = λ i a → ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a)  
     Λ CosColim-NatSq1 {i} {j} g = (λ x → ap-∘-rid φ₁ f (fst (comTri ColCoC g) x)) , λ a → lemma a
       where
         lemma : (a : A) → 
@@ -133,7 +133,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙
             ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙
             ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙
-            snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
+            snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
           long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙
             ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a)
             (ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙ -- here
@@ -143,7 +143,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
             (fst (comTri ColCoC g) (fun (F # i) a)) ∙
             ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
-          ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
+          ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
             =ₛ
           (ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j))
             (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙
@@ -165,7 +165,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙
             ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙
             ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙
-            snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
+            snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
           long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙
             ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a)
             (ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙
@@ -175,7 +175,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
             (fst (comTri ColCoC g) (fun (F # i) a)) ∙
             ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
-          ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
+          ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
             =ₛ⟨ 0 & 4 & NatSq-1-Λ-red g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a) ⟩
           ↯ (NatSq-1-Λ-aux g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a)) ◃∙ 
           ap (λ q → q) (ap-cp-revR φ₁ (f ∘ fst (comp ColCoC j)) (snd (F <#> g) a)
@@ -184,7 +184,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type 
             (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
             (fst (comTri ColCoC g) (fun (F # i) a)) ∙
             ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
-          ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
+          ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
             =ₛ⟨ NatSq-1-Λ-red2 g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (snd (comTri ColCoC g) a) ⟩          
           (ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j))
             (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙
diff --git a/Colimit-code/README.md b/Colimit-code/README.md
index a40194a..f2d21cd 100644
--- a/Colimit-code/README.md
+++ b/Colimit-code/README.md
@@ -50,7 +50,7 @@ check the entire development in a reasonable amount of time.
 
 ## Manual Type-Checking
 
-1. Install Agda 2.6.3.
+1. Install Agda 2.6.4.3.
 2. Install the stripped, modified HoTT-Agda library under `../HoTT-Agda`.
 3. Type-check the file `Main-Theorem/CosColim-Adjunction.agda`.
 
diff --git a/Dockerfile b/Dockerfile
index d3dac17..3b22924 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -6,8 +6,8 @@ ARG GHC_VERSION=9.4.7
 FROM fossa/haskell-static-alpine:ghc-${GHC_VERSION} AS agda
 
 WORKDIR /build/agda
-# Agda 2.6.3
-ARG AGDA_VERSION=b499d12412bac32ab1af9f470463ed9dc54f8907
+# Agda 2.6.4.3
+ARG AGDA_VERSION=714c7d2c76c5ffda3180e95c28669259f0dc5b5c
 RUN \
   git init && \
   git remote add origin https://github.com/agda/agda.git && \
diff --git a/HoTT-Agda/README.md b/HoTT-Agda/README.md
index c9cc8fb..842f400 100644
--- a/HoTT-Agda/README.md
+++ b/HoTT-Agda/README.md
@@ -10,7 +10,7 @@ lemmas. The structure of the source code is described below.
 Setup
 -----
 
-The library is compatible with Agda 2.6.3. To use it, you need a recent version of Agda and to include at
+The library is compatible with Agda 2.6.4.3. To use it, you need a recent version of Agda and to include at
 least the path to `hott-core.agda-lib` in your Agda library list.
 
 Agda Options
diff --git a/HoTT-Agda/core/lib/PathOver.agda b/HoTT-Agda/core/lib/PathOver.agda
index a20e710..52ea716 100644
--- a/HoTT-Agda/core/lib/PathOver.agda
+++ b/HoTT-Agda/core/lib/PathOver.agda
@@ -385,10 +385,10 @@ 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 = Σ (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) ◃∎
+  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  
@@ -396,11 +396,11 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where
   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))
+    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 ◃∎
+  snd (⊙id-to-comp idp) = idp
 
 {- Various other lemmas -}
 
diff --git a/HoTT-Agda/core/lib/types/Homogeneous.agda b/HoTT-Agda/core/lib/types/Homogeneous.agda
index 5a8e9dc..24e2542 100644
--- a/HoTT-Agda/core/lib/types/Homogeneous.agda
+++ b/HoTT-Agda/core/lib/types/Homogeneous.agda
@@ -46,7 +46,7 @@ module _ {i} {X : Type i} where
     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))
+        ↯ pathseq))
       where
         lemma : {m : ⊙[ X , f z ] ⊙→ ⊙[ X , f z ]} (τ : m == ⊙idf ⊙[ X , f z ]) 
           → ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap) τ) ∙ idp) ∙
@@ -117,58 +117,58 @@ module _ {i} {X : Type i} where
       ∼⊙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₁ₚ : ! (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₁
+          (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₂ₚ))))) ∙
+          (ap-post∙idp∘!-inv (H₁ₚ ∙ ! (H₂ₚ)))) ∙
         <–-inv-r (ap-equiv (post∙idp∘!-is-equiv) idp idp)
-          (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ)))))
+          (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₁ 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₂ₚ)) ◃∎}
+          {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₂ₚ)) ◃∎}
+            {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₂ₚ
+        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₂ₚ)) ◃∎}
+                 {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₂ₚ)) ◃∎}
+              {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₂ₚ
+         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₂ₚ)) ◃∎}
+                 {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)}
+                 {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)}
                  (ap λ= (λ= K)))) ⟩
-         H₁ₚ ∎ₛ
+         H₁ₚ ◃∎ ∎ₛ
 
 -- All loop spaces are coherently homogeneous.
 
@@ -183,12 +183,13 @@ module _ {i} {X : Type i} {x : X} where
     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 ◃∎))
+        !-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₁ (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/Pointed.agda b/HoTT-Agda/core/lib/types/Pointed.agda
index ee58a71..582ef22 100644
--- a/HoTT-Agda/core/lib/types/Pointed.agda
+++ b/HoTT-Agda/core/lib/types/Pointed.agda
@@ -60,27 +60,27 @@ module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} where
     → ((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) ◃∎
+    ! (∙-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))) ◃∎
+    ! (∙-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)) ◃∎
-
+    ! (∙-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 
@@ -89,9 +89,9 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} {f₁ f₂ f₃ : X ⊙→ Y} where
   _∙⊙∼_ : 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₃) ◃∎
+    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
 
@@ -100,16 +100,16 @@ 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))) ◃∎
+    ap (λ p → p ∙ snd f₂) (!-! (H₀ (pt (X)))) ∙
+    ap (λ p → H₀ (pt X) ∙ p) (! 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 ◃∎
+  snd (⊙∼-id (f , fₚ)) = idp
 
 -- homotopies of homotopies of pointed maps
 
@@ -119,7 +119,7 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where
   _⊙→∼_ : {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₁)
+      (λ K → ap (λ p →  ! p ∙ snd f) (K (pt X)) ◃∙ snd H₂ ◃∎ =ₛ snd H₁ ◃∎)
 
 -- pointed sections
 
diff --git a/HoTT-Agda/core/lib/types/Suspension.agda b/HoTT-Agda/core/lib/types/Suspension.agda
index 55d33d3..3175466 100644
--- a/HoTT-Agda/core/lib/types/Suspension.agda
+++ b/HoTT-Agda/core/lib/types/Suspension.agda
@@ -69,29 +69,29 @@ susp-⊙span X =
 
 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
+  (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 = 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 : 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)
+    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
+   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 (λ 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) ∙
+      (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))
@@ -104,9 +104,9 @@ module _ {i j} {A : Type i} {B : Type j} (f g : Susp A → 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-∙ 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) ∙
+      (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))
@@ -158,7 +158,7 @@ module _ {i j k} {X : Type i} {Y : Type j} {Z : Type k} (g : Y → Z) (f : X →
 
   Susp-fmap-∘-∼ =
     SuspMapEq (Susp-fmap (g ∘ f)) (Susp-fmap g ∘ Susp-fmap f) idp idp
-      (Susp-fmap-∘ g f)
+      (λ a → ↯ (Susp-fmap-∘ g f a))
 
 module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} (g : Y ⊙→ Z) (f : X ⊙→ Y) where
 
diff --git a/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda b/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda
index 0df4482..9092a17 100644
--- a/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda
+++ b/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda
@@ -53,7 +53,7 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where
             (! (∙-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))
@@ -67,9 +67,9 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where
           ap (λ p → ! (! u ∙ idp) ∙ idp ∙' p)
             (! (∙-unit-r (! u))) ∙ idp) ∙
           ! (Ω-fmap-β (g , ! u ∙ idp) idp)) ∙ idp
-          =-=
+          ==
           snd (⊙Ω-fmap (g , ! u ∙ idp))
-      lemma idp = 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ₚ)
@@ -82,7 +82,7 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where
         ∙-∙'-= (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))
 
@@ -93,9 +93,9 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where
         (! (!-! (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))) ∙
+      ∙-∙'-= (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))
+  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,
@@ -115,7 +115,7 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where
         ∙-unit-r (hmpty-nat-∙'-r (λ x₁ → idp) (v ∙ ! v)) ∙
         hmpty-nat-∙'-r-idp (v ∙ ! v)) ∙ idp
         ==
-        ↯ (ap-comp-into-coher-aux (λ x → idp) v)
+        ap-comp-into-coher-aux (λ x → idp) v
       lemma idp = idp
       
 {-
@@ -183,12 +183,12 @@ module _ {i i' j} {X : Ptd i} {Y : Ptd i'} {U : Ptd j} where
           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-∙ (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)))) ◃∎
+        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 -}
 
@@ -272,19 +272,19 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W :
 
     β-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)) ∙
+        (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) w)) ∙
       ap f₁ (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃)
-        idp idp (Susp-fmap-∘ f₂ f₃) w ∙
+        idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) 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)) →
+        idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) 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₃)) (! ω₆) ∙
+        idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (! ω₆) ∙
       𝕗 ∙ 
       ! (ap (ap f₁) (ap (λ q → q) (ap ! (! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₆)) ∙
         !-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₆) ∙ idp))
@@ -304,7 +304,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W :
       ! (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₃)) (ω₃ ∙ ! ω₆) ∙
+        idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (ω₃ ∙ ! ω₆) ∙
       ! (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₃) ω₆) ∙
@@ -336,7 +336,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W :
       ! (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₃)) (ω₃ ∙ ! ω₆) ∙
+        idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (ω₃ ∙ ! ω₆) ∙
       ! (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₃) ω₆)) ∙
@@ -517,7 +517,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W :
         ==
       ((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))) ∙
+        idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (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))))
@@ -537,7 +537,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W :
         (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))
+      (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) f₁ x (pt W))
 
     -- proof of 2-coherence
 
@@ -546,7 +546,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {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))))
+        idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (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)))
@@ -634,7 +634,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W :
     ⊙∘-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 ◃∎))) ∙⊙∼
+      ⊙∘-post h₁ (!-⊙∼ (Susp-fmap-∘-∼ (fst h₂) (fst h₃) , idp))) ∙⊙∼
     !-⊙∼ (nat-dom (h₂ ⊙∘ h₃) h₁)
       ⊙→∼
     ⊙∼-id ((into X Y h₁) ⊙∘ h₂ ⊙∘ h₃)
diff --git a/Pullback-stability/README.md b/Pullback-stability/README.md
index 8276905..b0ad211 100644
--- a/Pullback-stability/README.md
+++ b/Pullback-stability/README.md
@@ -9,7 +9,7 @@ Theorem 16 of our preprint).
 
 ## Manual Type-Checking
 
-1. Install Agda 2.6.3.
+1. Install Agda 2.6.4.3.
 2. Install the stripped, modified HoTT-Agda library under `../HoTT-Agda`.
 3. Install the library under `../Colimit-code`.
 3. Type check the file `Stability.agda`.
diff --git a/README.md b/README.md
index eda40b0..41c83be 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 ## Overview
 
   This Agda code accompanies our paper [Coslice Colimits in Homotopy Type Theory](https://phart3.github.io/colimits-paper.pdf).
-  (The link points to the preprint.) It has been checked with Agda 2.6.3.
+  (The link points to the preprint.) It has been checked with Agda 2.6.4.3.
 
 ## Organization