diff --git a/src/foundation-core/universal-property-pullbacks.lagda.md b/src/foundation-core/universal-property-pullbacks.lagda.md
index 6d448cda3c..8e7a7c9f75 100644
--- a/src/foundation-core/universal-property-pullbacks.lagda.md
+++ b/src/foundation-core/universal-property-pullbacks.lagda.md
@@ -50,11 +50,11 @@ module _
   map-universal-property-pullback up-c {C'} c' =
     map-inv-is-equiv (up-c C') c'
 
-  eq-map-universal-property-pullback :
+  compute-map-universal-property-pullback :
     (up-c : {l : Level} → universal-property-pullback l f g c) →
     {C' : UU l5} (c' : cone f g C') →
     cone-map f g c (map-universal-property-pullback up-c c') ＝ c'
-  eq-map-universal-property-pullback up-c {C'} c' =
+  compute-map-universal-property-pullback up-c {C'} c' =
     is-section-map-inv-is-equiv (up-c C') c'
 ```
 
diff --git a/src/foundation/cones-over-cospans.lagda.md b/src/foundation/cones-over-cospans.lagda.md
index 6601d6e59f..65a6e5a8ed 100644
--- a/src/foundation/cones-over-cospans.lagda.md
+++ b/src/foundation/cones-over-cospans.lagda.md
@@ -27,7 +27,7 @@ open import foundation-core.whiskering-homotopies
 
 ## Idea
 
-A **cone on a [cospan](foundation.cospans.md)** `A -f-> X <-g- B` with domain
+A **cone over a [cospan](foundation.cospans.md)** `A -f-> X <-g- B` with domain
 `C` is a triple `(p, q, H)` consisting of a map `p : C → A`, a map `q : C → B`,
 and a homotopy `H` witnessing that the square
 
diff --git a/src/foundation/towers.lagda.md b/src/foundation/towers.lagda.md
index ce12daef18..da4966c9b6 100644
--- a/src/foundation/towers.lagda.md
+++ b/src/foundation/towers.lagda.md
@@ -19,7 +19,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **tower of types** `f` is a [sequence](foundation.sequences.md) of types
+A **tower of types** `A` is a [sequence](foundation.sequences.md) of types
 together with maps between every two consecutive types
 
 ```text
diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md
index 4ad9c94f17..73c8bfbbf0 100644
--- a/src/foundation/universal-property-pullbacks.lagda.md
+++ b/src/foundation/universal-property-pullbacks.lagda.md
@@ -80,7 +80,7 @@ module _
     htpy-eq-cone f g
       ( cone-map f g c (map-universal-property-pullback f g c up c'))
       ( c')
-      ( eq-map-universal-property-pullback f g c up c')
+      ( compute-map-universal-property-pullback f g c up c')
 ```
 
 ### Uniquely uniqueness of pullbacks
diff --git a/src/foundation/universal-property-sequential-limits.lagda.md b/src/foundation/universal-property-sequential-limits.lagda.md
index a2367b7edc..e9eac427f1 100644
--- a/src/foundation/universal-property-sequential-limits.lagda.md
+++ b/src/foundation/universal-property-sequential-limits.lagda.md
@@ -73,11 +73,11 @@ module _
   map-universal-property-sequential-limit up-c {Y} c' =
     map-inv-is-equiv (up-c Y) c'
 
-  eq-map-universal-property-sequential-limit :
+  compute-map-universal-property-sequential-limit :
     (up-c : {l : Level} → universal-property-sequential-limit l A c) →
     {Y : UU l3} (c' : cone-tower A Y) →
     cone-map-tower A c (map-universal-property-sequential-limit up-c c') ＝ c'
-  eq-map-universal-property-sequential-limit up-c {Y} c' =
+  compute-map-universal-property-sequential-limit up-c {Y} c' =
     is-section-map-inv-is-equiv (up-c Y) c'
 ```
 
@@ -206,7 +206,7 @@ module _
     htpy-eq-cone-tower A
       ( cone-map-tower A c (map-universal-property-sequential-limit A c up c'))
       ( c')
-      ( eq-map-universal-property-sequential-limit A c up c')
+      ( compute-map-universal-property-sequential-limit A c up c')
 ```
 
 ### Unique uniqueness of sequential limits