diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md
index 36b262e97b..cd859525e3 100644
--- a/src/foundation/commuting-squares-of-maps.lagda.md
+++ b/src/foundation/commuting-squares-of-maps.lagda.md
@@ -1004,37 +1004,3 @@ module _
     ( h) =
     compute-concat-htpy-precomp H K W h
 ```
-
-### Naturality of `eq-htpy` for ordinary functions
-
-Consider a map `f : A → B` and two functions `g h : B → C`. Then the square
-
-```text
-                     ap (precomp f C)
-       (g ＝ h) -------------------------> (g ∘ f ＝ h ∘ f)
-          ^                                       ^
-  eq-htpy |                                       | eq-htpy
-          |                                       |
-       (g ~ h) --------------------------> (g ∘ f ~ h ∘ f)
-                precomp f (eq-value g h)
-```
-
-commutes.
-
-```agda
-square-eq-htpy :
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
-  (f : A → B) (g h : B → C) →
-  coherence-square-maps
-    ( precomp-Π f (eq-value g h))
-    ( eq-htpy)
-    ( eq-htpy)
-    ( ap (precomp f C))
-square-eq-htpy {C = C} f g h =
-  coherence-square-inv-vertical
-    ( ap (precomp f C))
-    ( equiv-funext)
-    ( equiv-funext)
-    ( precomp-Π f (eq-value g h))
-    ( square-htpy-eq f g h)
-```