chore: update reference to eso→pre-faithful in Hott.lagda.md

the1lab · Nov 25, 2024 · 101b2ee · 101b2ee
1 parent 80f3c36
commit 101b2ee
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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→pre-faithful
+_ = eso→precompose-faithful
 _ = eso-full→pre-ff
 _ = Rezk-completion
 _ = complete-is-eso
@@ -1009,7 +1009,7 @@ _ = complete
 ```
 -->
 
-* Lemma 9.9.1: `eso→pre-faithful`{.Agda}
+* Lemma 9.9.1: `eso→precompose-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}.