From 5327f959f740fcb5a27eeb571be541a6bff00a4a Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Tue, 5 Dec 2023 10:38:48 -0500
Subject: [PATCH] Typos in the universal property of the family of fibers of a
 map (#971)

---
 ...property-family-of-fibers-of-maps.lagda.md | 25 +++++++++++--------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
index 18d9ea9e3b..fa50fc60b7 100644
--- a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
+++ b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
@@ -1,4 +1,4 @@
-# The universal property of family of fibers of maps
+# The universal property of the family of fibers of maps
 
 ```agda
 module foundation.universal-property-family-of-fibers-of-maps where
@@ -79,7 +79,7 @@ described above, while the universal property of the fiber `fiber f b` of a map
 
 ## Definitions
 
-### The dependent universal property of the fibers of a map
+### The dependent universal property of the family of fibers of a map
 
 Consider a map `f : A → B` and a type family `F : B → 𝒰` equipped with a lift
 `δ : (a : A) → F (f a)` of `f` to `F`. Then there is an evaluation map
@@ -89,9 +89,11 @@ Consider a map `f : A → B` and a type family `F : B → 𝒰` equipped with a
 ```
 
 for any binary type family `X : (b : B) → F b → 𝒰`. This evaluation map takes a
-binary family of elements of `X` to a double lift over `f` and `δ`. The
-dependent universal property of the family of fibers of `f` asserts that this
-evaluation map is an equivalence.
+binary family of elements of `X` to a
+[double lift](orthogonal-factorization-systems.double-lifts-families-of-elements.md)
+of `f` and `δ`. The
+{{#concept "dependent universal property of the family of fibers of a map"}} `f`
+asserts that this evaluation map is an equivalence.
 
 ```agda
 module _
@@ -105,18 +107,19 @@ module _
     is-equiv (ev-double-lift-family-of-elements {B = F} δ {X})
 ```
 
-### The universal property of the fibers of a map
+### The universal property of the family of fibers of a map
 
 Consider a map `f : A → B` and a type family `F : B → 𝒰` equipped with a lift
-`δ : (a : A) → F (f f)` of `f` to `F`. Then there is an evaluation map
+`δ : (a : A) → F (f a)` of `f` to `F`. Then there is an evaluation map
 
 ```text
   ((b : B) → F b → X b) → ((a : A) → X (f a))
 ```
 
 for any binary type family `X : B → 𝒰`. This evaluation map takes a binary
-family of elements of `X` to a lift of `f`. The universal property of the family
-of fibers of `f` asserts that this evaluation map is an equivalence.
+family of elements of `X` to a double lift of `f` and `δ`. The universal
+property of the family of fibers of `f` asserts that this evaluation map is an
+equivalence.
 
 ```agda
 module _
@@ -221,7 +224,7 @@ module _
     dependent-universal-property-family-of-fibers-fiber C
 ```
 
-### The family of fibers of a map satisfies the dependent universal property of the family of fibers of a map
+### The family of fibers of a map satisfies the universal property of the family of fibers of a map
 
 ```agda
 module _
@@ -300,7 +303,7 @@ module _
       extension-universal-property-family-of-fibers
 ```
 
-### Fibers are uniquely unique
+### The family of fibers of a map is uniquely unique
 
 ```agda
 module _