diff --git a/src/foundation-core/commuting-prisms-of-maps.lagda.md b/src/foundation-core/commuting-prisms-of-maps.lagda.md
index a71ff6b45e..86888cf6a8 100644
--- a/src/foundation-core/commuting-prisms-of-maps.lagda.md
+++ b/src/foundation-core/commuting-prisms-of-maps.lagda.md
@@ -189,7 +189,11 @@ module _
       ( (hC ·l inv-top) ∙h inv-front)
 ```
 
-## Translations
+## Translations between coherences of prisms of maps
+
+Our different formulations of commuting prisms of maps are of course all
+equivalent, although this remains to be formalized. Below, we record various
+translations between them.
 
 ```agda
 module _
diff --git a/src/foundation/commuting-prisms-of-maps.lagda.md b/src/foundation/commuting-prisms-of-maps.lagda.md
index 95bc495af4..5401d5e158 100644
--- a/src/foundation/commuting-prisms-of-maps.lagda.md
+++ b/src/foundation/commuting-prisms-of-maps.lagda.md
@@ -183,6 +183,8 @@ module _
 
 ### Commuting prisms of maps induces commuting prisms on function types via precomposition
 
+We prove this for a few different formulations of commuting prisms of maps.
+
 ```agda
 module _
   { l1 l2 l3 l1' l2' l3' l : Level}
diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-maps.lagda.md
index 1fcdd1b73a..1939ca1ad0 100644
--- a/src/foundation/retracts-of-maps.lagda.md
+++ b/src/foundation/retracts-of-maps.lagda.md
@@ -77,6 +77,20 @@ witnessing that the
 where `H₀` and `H₁` are the retracting homotopies of `r₀ ∘ i₀` and `r₁ ∘ i₁`
 respectively.
 
+This coherence arises from the implicit requirement that the total pasting of
+the retraction square should restrict the the reflixivity homotopy on the square
+
+```text
+    A ========= A
+    |           |
+  f | refl-htpy | f
+    v           v
+    B ========= B,
+```
+
+as we are asking for the morphisms to compose to the identity morphism of
+arrows.
+
 ## Definition
 
 ### The predicate of being a retraction of a morphism of arrows
@@ -144,28 +158,6 @@ module _
   coherence-retract-map : UU (l1 ⊔ l2)
   coherence-retract-map =
     coherence-htpy-hom-arrow f f (comp-hom-arrow f g f r i) id-hom-arrow H H'
-
-  coherence-prism-retract-map : UU (l1 ⊔ l2)
-  coherence-prism-retract-map =
-    vertical-coherence-prism-inv-triangles-maps
-      ( id)
-      ( map-domain-hom-arrow g f r)
-      ( map-domain-hom-arrow f g i)
-      ( id)
-      ( map-codomain-hom-arrow g f r)
-      ( map-codomain-hom-arrow f g i)
-      ( f)
-      ( g)
-      ( f)
-      ( H)
-      ( refl-htpy)
-      ( coh-hom-arrow g f r)
-      ( coh-hom-arrow f g i)
-      ( H')
-
-  eq-coherence-retract-map-coherence-prism-retract-map :
-    coherence-prism-retract-map ＝ coherence-retract-map
-  eq-coherence-retract-map-coherence-prism-retract-map = refl
 ```
 
 ### The binary relation `f g ↦ f retract-of-map g` asserting that `f` is a retract of the map `g`
@@ -410,7 +402,7 @@ module _
 
 ### Equivalences are closed under retracts of maps
 
-Note that the higher coherence of a retract of maps is not needed.
+We may observe that the higher coherence of a retract of maps is not needed.
 
 ```agda
 module _
diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/local-types.lagda.md
index 7b38fbe7ad..7cf28a31d3 100644
--- a/src/orthogonal-factorization-systems/local-types.lagda.md
+++ b/src/orthogonal-factorization-systems/local-types.lagda.md
@@ -241,7 +241,7 @@ is-contr-is-local A is-local-A =
     ( universal-property-empty' A)
 ```
 
-### If `S` is `g`-local, and `f` is a retract of `g`, then `S` is also `f`-local
+### If `S` is `g`-local, and `f` is a retract of `g` then `S` is `f`-local
 
 ```agda
 module _