Fix "The predicate of" section headers (#1010)

This PR gives section headers that start as "The predicate ..." a uniform appearance: - Sentences of the form "The predicate of ... on ..." are changed to "The predicate on ... of ...". - Predicates are not on single elements of types, so in cases where this was suggested I reformulated it to plural.
UniMath · Jan 27, 2024 · de23cc1 · de23cc1
1 parent 6e87c58
commit de23cc1
Show file tree

Hide file tree

Showing 26 changed files with 34 additions and 34 deletions.
diff --git a/src/category-theory/embedding-maps-precategories.lagda.md b/src/category-theory/embedding-maps-precategories.lagda.md
@@ -36,7 +36,7 @@ considered in
 
 ## Definition
 
-### The predicate of being an embedding map on maps between precategories
+### The predicate on maps between precategories of being an embedding map
 
 ```agda
 module _

diff --git a/src/category-theory/embeddings-precategories.lagda.md b/src/category-theory/embeddings-precategories.lagda.md
@@ -31,7 +31,7 @@ hom-[sets](foundation-core.sets.md).
 
 ## Definition
 
-### The predicate of being an embedding on maps between precategories
+### The predicate on maps between precategories of being an embedding
 
 ```agda
 module _
@@ -56,7 +56,7 @@ module _
     is-prop-type-Prop is-embedding-prop-map-Precategory
 ```
 
-### The predicate of being an embedding on functors between precategories
+### The predicate on functors between precategories of being an embedding
 
 ```agda
 module _

diff --git a/src/category-theory/faithful-functors-precategories.lagda.md b/src/category-theory/faithful-functors-precategories.lagda.md
@@ -34,7 +34,7 @@ in terms of embeddings because this is the notion that generalizes.
 
 ## Definition
 
-### The predicate of being faithful on functors between precategories
+### The predicate on functors between precategories of being faithful
 
 ```agda
 module _
@@ -95,7 +95,7 @@ module _
     hom-functor-Precategory C D functor-faithful-functor-Precategory
 ```
 
-### The predicate of being injective on hom-sets on functors between precategories
+### The predicate on functors between precategories of being injective on hom-sets
 
 ```agda
 module _

diff --git a/src/category-theory/faithful-maps-precategories.lagda.md b/src/category-theory/faithful-maps-precategories.lagda.md
@@ -34,7 +34,7 @@ stronger notion, as this is the notion that generalizes.
 
 ## Definition
 
-### The predicate of being faithful on maps between precategories
+### The predicate on maps between precategories of being faithful
 
 ```agda
 module _
@@ -95,7 +95,7 @@ module _
     hom-map-Precategory C D ∘ map-faithful-map-Precategory
 ```
 
-### The predicate of being injective on hom-sets on maps between precategories
+### The predicate on maps between precategories of being injective on hom-sets
 
 ```agda
 module _

diff --git a/src/category-theory/full-functors-precategories.lagda.md b/src/category-theory/full-functors-precategories.lagda.md
@@ -28,7 +28,7 @@ hom-[sets](foundation-core.sets.md).
 
 ## Definition
 
-### The predicate of being full on functors between precategories
+### The predicate on functors between precategories of being full
 
 ```agda
 module _

diff --git a/src/category-theory/full-maps-precategories.lagda.md b/src/category-theory/full-maps-precategories.lagda.md
@@ -29,7 +29,7 @@ hom-[sets](foundation-core.sets.md).
 
 ## Definition
 
-### The predicate of being full on maps between precategories
+### The predicate on maps between precategories of being full
 
 ```agda
 module _

diff --git a/src/category-theory/fully-faithful-functors-precategories.lagda.md b/src/category-theory/fully-faithful-functors-precategories.lagda.md
@@ -44,7 +44,7 @@ precategories.
 
 ## Definitions
 
-### The predicate of being fully faithful on functors between precategories
+### The predicate on functors between precategories of being fully faithful
 
 ```agda
 module _

diff --git a/src/category-theory/fully-faithful-maps-precategories.lagda.md b/src/category-theory/fully-faithful-maps-precategories.lagda.md
@@ -34,7 +34,7 @@ precategories.
 
 ## Definition
 
-### The predicate of being fully faithful on maps between precategories
+### The predicate on maps between precategories of being fully faithful
 
 ```agda
 module _

diff --git a/src/category-theory/functors-categories.lagda.md b/src/category-theory/functors-categories.lagda.md
@@ -30,7 +30,7 @@ A **functor** between two [categories](category-theory.categories.md) is a
 
 ## Definition
 
-### The predicate of being a functor on maps between categories
+### The predicate on maps between categories of being a functor
 
 ```agda
 module _

diff --git a/src/category-theory/functors-from-small-to-large-categories.lagda.md b/src/category-theory/functors-from-small-to-large-categories.lagda.md
@@ -34,7 +34,7 @@ A **functor** from a [(small) category](category-theory.categories.md) `C` to a
 
 ## Definition
 
-### The predicate of being a functor on maps from small to large categories
+### The predicate on maps from small to large categories of being a functor
 
 ```agda
 module _

diff --git a/src/category-theory/functors-from-small-to-large-precategories.lagda.md b/src/category-theory/functors-from-small-to-large-precategories.lagda.md
@@ -37,7 +37,7 @@ of:
 
 ## Definition
 
-### The predicate of being a functor on maps from small to large precategories
+### The predicate on maps from small to large precategories of being a functor
 
 ```agda
 module _

diff --git a/src/category-theory/functors-precategories.lagda.md b/src/category-theory/functors-precategories.lagda.md
@@ -40,7 +40,7 @@ precategory `D` consists of:
 
 ## Definition
 
-### The predicate of being a functor on maps between precategories
+### The predicate on maps between precategories of being a functor
 
 ```agda
 module _

diff --git a/src/category-theory/precategories.lagda.md b/src/category-theory/precategories.lagda.md
@@ -44,7 +44,7 @@ identities between the objects are exactly the isomorphisms.
 
 ## Definitions
 
-### The predicate of being a precategory on composition operations on binary families of sets
+### The predicate on composition operations on binary families of sets of being a precategory
 
 ```agda
 module _

diff --git a/src/category-theory/pregroupoids.lagda.md b/src/category-theory/pregroupoids.lagda.md
@@ -30,7 +30,7 @@ every morphism is an
 
 ## Definitions
 
-### The predicate on precategories of being pregroupoids
+### The predicate on precategories of being a pregroupoid
 
 ```agda
 module _

diff --git a/src/category-theory/subcategories.lagda.md b/src/category-theory/subcategories.lagda.md
@@ -215,7 +215,7 @@ module _
     inclusion-subtype (subtype-hom-obj-subcategory-Subcategory x y)
 ```
 
-The predicate on a morphism between subobjects of being contained in the
+The predicate on morphisms between subobjects of being contained in the
 subcategory:
 
 ```agda
@@ -239,7 +239,7 @@ subcategory:
     is-prop-is-in-subtype (subtype-hom-obj-subcategory-Subcategory x y)
 ```
 
-The predicate on a morphism between any objects of being contained in the
+The predicate on morphisms between any objects of being contained in the
 subcategory:
 
 ```agda

diff --git a/src/category-theory/subprecategories.lagda.md b/src/category-theory/subprecategories.lagda.md
@@ -225,7 +225,7 @@ module _
     inclusion-subtype (subtype-hom-obj-subprecategory-Subprecategory x y)
 ```
 
-The predicate on a morphism between subobjects of being contained in the
+The predicate on morphisms between subobjects of being contained in the
 subprecategory:
 
 ```agda
@@ -249,7 +249,7 @@ subprecategory:
     is-prop-is-in-subtype (subtype-hom-obj-subprecategory-Subprecategory x y)
 ```
 
-The predicate on a morphism between any objects of being contained in the
+The predicate on morphisms between any objects of being contained in the
 subprecategory:
 
 ```agda

diff --git a/src/category-theory/subterminal-precategories.lagda.md b/src/category-theory/subterminal-precategories.lagda.md
@@ -43,7 +43,7 @@ A [precategory](category-theory.precategories.md) is **subterminal** if its
 
 ## Definitions
 
-### The predicate of being subterminal on precategories
+### The predicate on precategories of being subterminal
 
 ```agda
 module _

diff --git a/src/category-theory/wide-subcategories.lagda.md b/src/category-theory/wide-subcategories.lagda.md
@@ -148,7 +148,7 @@ module _
     is-prop-is-closed-under-composition-subtype-hom-wide-Category
 ```
 
-### The predicate on a subtype of the hom-sets of being a wide subcategory
+### The predicate on subtypes of hom-sets of being a wide subcategory
 
 ```agda
 module _
@@ -236,7 +236,7 @@ module _
     inclusion-subtype (subtype-hom-Wide-Subcategory x y)
 ```
 
-The predicate on a morphism between any objects of being contained in the wide
+The predicate on morphisms between any objects of being contained in the wide
 subcategory:
 
 ```agda

diff --git a/src/category-theory/wide-subprecategories.lagda.md b/src/category-theory/wide-subprecategories.lagda.md
@@ -115,7 +115,7 @@ module _
     is-prop-is-closed-under-composition-subtype-hom-wide-Precategory
 ```
 
-### The predicate on a subtype of the hom-sets of being a wide subprecategory
+### The predicate on subtypes of hom-sets of being a wide subprecategory
 
 ```agda
 module _
@@ -203,7 +203,7 @@ module _
     inclusion-subtype (subtype-hom-Wide-Subprecategory x y)
 ```
 
-The predicate on a morphism between any objects of being contained in the wide
+The predicate on morphisms between any objects of being contained in the wide
 subprecategory:
 
 ```agda

diff --git a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md
@@ -33,7 +33,7 @@ open import foundation.universe-levels
 
 ## Definition
 
-### The predicate `is-gcd-ℤ`
+### The predicate of being a greatest common divisor
 
 ```agda
 is-common-divisor-ℤ : ℤ → ℤ → ℤ → UU lzero

diff --git a/src/foundation/global-subuniverses.lagda.md b/src/foundation/global-subuniverses.lagda.md
@@ -30,7 +30,7 @@ for homogeneous equivalences, i.e. equivalences in a single universe.
 
 ## Definitions
 
-### The predicate on a family of subuniverses of being closed under equivalences
+### The predicate on families of subuniverses of being closed under equivalences
 
 ```agda
 module _

diff --git a/src/order-theory/large-posets.lagda.md b/src/order-theory/large-posets.lagda.md
@@ -86,7 +86,7 @@ module _
     transitive-leq-Large-Preorder (large-preorder-Large-Poset X)
 ```
 
-### The predicate on a large category of being a large poset
+### The predicate on large categories of being a large poset
 
 A [large category](category-theory.large-categories.md) is said to be a **large
 poset** if `hom X Y` is a proposition for every two objects `X` and `Y`.

diff --git a/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md b/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md
@@ -43,7 +43,7 @@ map of the factorization.
 
 ## Definitions
 
-### The predicate on a triangle of maps of being a factorization
+### The predicate on triangles of maps of being a factorization
 
 ```agda
 module _

diff --git a/src/orthogonal-factorization-systems/global-function-classes.lagda.md b/src/orthogonal-factorization-systems/global-function-classes.lagda.md
@@ -33,7 +33,7 @@ correct universe polymorphic definition.
 
 ## Definitions
 
-### The predicate on a family of function classes of being closed under composition with equivalences
+### The predicate on families of function classes of being closed under composition with equivalences
 
 ```agda
 module _

diff --git a/src/orthogonal-factorization-systems/wide-function-classes.lagda.md b/src/orthogonal-factorization-systems/wide-function-classes.lagda.md
@@ -28,7 +28,7 @@ and is composition closed. This means it is morally a wide sub-∞-category of t
 
 ## Definition
 
-### The predicate on a small function class of being wide
+### The predicate on small function classes of being wide
 
 ```agda
 module _

diff --git a/src/ring-theory/homomorphisms-rings.lagda.md b/src/ring-theory/homomorphisms-rings.lagda.md
@@ -37,7 +37,7 @@ Ring homomorphisms are maps between rings that preserve the ring structure
 
 ## Definitions
 
-### The predicate that a group homomorphism between rings preserves multiplication
+### The predicate on group homomorphisms between rings of preserving multiplication
 
 ```agda
 preserves-mul-hom-Ab :
@@ -66,7 +66,7 @@ is-prop-preserves-mul-hom-Ab R S f =
               ( map-hom-Ab (ab-Ring R) (ab-Ring S) f y))))
 ```
 
-### The predicate that a group homomorphism between rings preserves the unit
+### The predicate on group homomorphisms between rings of preserving the unit
 
 ```agda
 preserves-unit-hom-Ab :