diff --git a/src/Cat/Functor/Properties.lagda.md b/src/Cat/Functor/Properties.lagda.md
index cf713cb17..1c12705fb 100644
--- a/src/Cat/Functor/Properties.lagda.md
+++ b/src/Cat/Functor/Properties.lagda.md
@@ -231,7 +231,7 @@ precomposition functor $(-) \circ F : [\cD,\cA] \to [\cC,\cA]$ is faithful
 for every precategory $\cA$.
 
 ```agda
-  eso→precompose-faithful
+  is-eso→precompose-is-faithful
     : ∀ {oa ℓa} {A : Precategory oa ℓa}
     → (F : Functor C D)
     → is-eso F
@@ -250,7 +250,7 @@ $F$ doesn't miss out on any objects of $d$, but the actual proof involves
 some rather tedious calculations.
 </summary>
 ```agda
-  eso→precompose-faithful {A = A} F F-eso {G} {H} {α} {β} αL=βL =
+  is-eso→precompose-is-faithful {A = A} F F-eso {G} {H} {α} {β} αL=βL =
     ext λ d → ∥-∥-out! do
       (c , Fc≅d) ← F-eso d
       let module Fc≅d = D._≅_ Fc≅d
diff --git a/src/Cat/Univalent/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md
index 5273fd0f2..ab9961119 100644
--- a/src/Cat/Univalent/Rezk/Universal.lagda.md
+++ b/src/Cat/Univalent/Rezk/Universal.lagda.md
@@ -71,7 +71,7 @@ category]], then $- \circ H$ is essentially surjective. By the principle
 of unique choice, it is an equivalence, and thus^[since both its domain
 and codomain are univalent] an isomorphism.
 
-Luckily, we `already know`{.Agda ident=eso→precompose-faithful} that precomposition
+Luckily, we `already know`{.Agda ident=is-eso→precompose-is-faithful} that precomposition
 with an eso functor extends to a faithful functor. Unfortunately, the
 remaining two steps are both _quite_ technical: that's because we're given
 some _mere_^[truncated] data, from the assumption that $H$ is a weak
@@ -269,7 +269,7 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful.
   res =
     full+faithful→ff (precompose H)
       full
-      (eso→precompose-faithful H H-eso)
+      (is-eso→precompose-is-faithful H H-eso)
 ```
 
 ## Essential surjectivity
diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md
index c03d709c7..76e6aa23e 100644
--- a/src/HoTT.lagda.md
+++ b/src/HoTT.lagda.md
@@ -1000,7 +1000,7 @@ _ = Displayed
 _ = Rezk-completion-is-category
 _ = weak-equiv→pre-equiv
 _ = weak-equiv→pre-iso
-_ = eso→precompose-faithful
+_ = is-eso→precompose-is-faithful
 _ = eso-full→pre-ff
 _ = Rezk-completion
 _ = complete-is-eso
@@ -1009,7 +1009,7 @@ _ = complete
 ```
 -->
 
-* Lemma 9.9.1: `eso→precompose-faithful`{.Agda}
+* Lemma 9.9.1: `is-eso→precompose-is-faithful`{.Agda}
 * Lemma 9.9.2: `eso-full→pre-ff`{.Agda}
 * Lemma 9.9.4: `weak-equiv→pre-equiv`{.Agda}, `weak-equiv→pre-iso`{.Agda}
 * Theorem 9.9.5: `Rezk-completion`{.Agda}, `Rezk-completion-is-category`{.Agda}, `complete`{.Agda}, `complete-is-ff`{.Agda}, `complete-is-eso`{.Agda}.