diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md
index e6afc47890..50a5befa1e 100644
--- a/src/foundation/universal-property-fiber-products.lagda.md
+++ b/src/foundation/universal-property-fiber-products.lagda.md
@@ -28,9 +28,9 @@ open import foundation-core.universal-property-pullbacks
 
 ## Idea
 
-The {{#concept "fiberwise product" Disambiguation="types"}} of two families `P` and `Q` over a type `X` is the
-family of types `(P x) × (Q x)` over `X`. Similarly, the fiber product of two
-maps `f : A → X` and `g : B → X` is the type
+The {{#concept "fiberwise product" Disambiguation="types"}} of two families `P`
+and `Q` over a type `X` is the family of types `(P x) × (Q x)` over `X`.
+Similarly, the fiber product of two maps `f : A → X` and `g : B → X` is the type
 `Σ X (λ x → fiber f x × fiber g x)`, which fits in a
 [pullback](foundation-core.pullbacks.md) diagram on `f` and `g`.
 
diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md
index a6c881fe0b..1599b9b791 100644
--- a/src/foundation/universal-property-image.lagda.md
+++ b/src/foundation/universal-property-image.lagda.md
@@ -39,8 +39,9 @@ open import foundation-core.whiskering-homotopies
 
 ## Idea
 
-The {{#concept "image" Disambiguation="maps of types" Agda=is-image}} of a map `f : A → X` is the least
-[subtype](foundation-core.subtypes.md) of `X` containing all the values of `f`.
+The {{#concept "image" Disambiguation="maps of types" Agda=is-image}} of a map
+`f : A → X` is the least [subtype](foundation-core.subtypes.md) of `X`
+containing all the values of `f`.
 
 ## Definition
 
diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md
index e506ee07d6..b92212ebbc 100644
--- a/src/foundation/universal-property-propositional-truncation.lagda.md
+++ b/src/foundation/universal-property-propositional-truncation.lagda.md
@@ -36,9 +36,11 @@ open import foundation-core.type-theoretic-principle-of-choice
 ## Idea
 
 A map `f : A → P` into a [proposition](foundation-core.propositions.md) `P` is
-said to satisfy the {{#concept "universal property of the propositional truncation" Agda=universal-property-propositional-truncation}} of
-`A`, or is said to be a {{#concept "propositional truncation" Agda=is-propositional-truncation}} of `A`, if any map
-`g : A → Q` into a proposition `Q` extends uniquely along `f`.
+said to satisfy the
+{{#concept "universal property of the propositional truncation" Agda=universal-property-propositional-truncation}}
+of `A`, or is said to be a
+{{#concept "propositional truncation" Agda=is-propositional-truncation}} of `A`,
+if any map `g : A → Q` into a proposition `Q` extends uniquely along `f`.
 
 ## Definition