pre-commit

UniMath · Dec 10, 2023 · 08aa0d2 · 08aa0d2
1 parent 85d1f4b
commit 08aa0d2
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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