From de23cc122ee1526c1cd82f020304898fbcd66624 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sat, 27 Jan 2024 12:14:23 +0100 Subject: [PATCH] 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. --- src/category-theory/embedding-maps-precategories.lagda.md | 2 +- src/category-theory/embeddings-precategories.lagda.md | 4 ++-- src/category-theory/faithful-functors-precategories.lagda.md | 4 ++-- src/category-theory/faithful-maps-precategories.lagda.md | 4 ++-- src/category-theory/full-functors-precategories.lagda.md | 2 +- src/category-theory/full-maps-precategories.lagda.md | 2 +- .../fully-faithful-functors-precategories.lagda.md | 2 +- .../fully-faithful-maps-precategories.lagda.md | 2 +- src/category-theory/functors-categories.lagda.md | 2 +- .../functors-from-small-to-large-categories.lagda.md | 2 +- .../functors-from-small-to-large-precategories.lagda.md | 2 +- src/category-theory/functors-precategories.lagda.md | 2 +- src/category-theory/precategories.lagda.md | 2 +- src/category-theory/pregroupoids.lagda.md | 2 +- src/category-theory/subcategories.lagda.md | 4 ++-- src/category-theory/subprecategories.lagda.md | 4 ++-- src/category-theory/subterminal-precategories.lagda.md | 2 +- src/category-theory/wide-subcategories.lagda.md | 4 ++-- src/category-theory/wide-subprecategories.lagda.md | 4 ++-- .../greatest-common-divisor-integers.lagda.md | 2 +- src/foundation/global-subuniverses.lagda.md | 2 +- src/order-theory/large-posets.lagda.md | 2 +- .../factorizations-of-maps.lagda.md | 2 +- .../global-function-classes.lagda.md | 2 +- .../wide-function-classes.lagda.md | 2 +- src/ring-theory/homomorphisms-rings.lagda.md | 4 ++-- 26 files changed, 34 insertions(+), 34 deletions(-) diff --git a/src/category-theory/embedding-maps-precategories.lagda.md b/src/category-theory/embedding-maps-precategories.lagda.md index 8212659c8a..17607bf873 100644 --- 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 index 65b93ae7bf..5361a0bb8c 100644 --- 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 index 19f3dbe2e4..8c6ea55099 100644 --- 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 index 2fcbc71d8c..40b26f802d 100644 --- 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 index eae23c838f..6fcd4a2690 100644 --- 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 index 06d6cef6ce..8b9755fe96 100644 --- 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 index 91f8f86df4..a0de4952c0 100644 --- 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 index 2e532d64a4..3716c27af4 100644 --- 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 index 97d1b4e815..8b751210a5 100644 --- 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 index c8bead03b1..0194f3b8dd 100644 --- 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 index c07203e98e..0565ce0d40 100644 --- 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 index e0617936d4..278355a77c 100644 --- 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 index 1c06110b87..6065725129 100644 --- 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 index 8e0357c6a1..baf074016f 100644 --- 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 index 91e26f7397..1f4f0b33e8 100644 --- 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 index 1c94b7ac92..489037b0a1 100644 --- 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 index 124025252f..232425c38b 100644 --- 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 index 2e630473c1..67bc98e8c1 100644 --- 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 index c7b16ea19e..fa7d767084 100644 --- 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 index 2dc2e9236a..d8fb62a832 100644 --- 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 index a2902c6d30..cb61c27018 100644 --- 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 index 18b3359ba2..53eca4adda 100644 --- 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 index 9eca2a16c8..6ce6c158b2 100644 --- 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 index f8bd583ee6..3453efac02 100644 --- 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 index aaff32a67f..a9af0f0d18 100644 --- 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 index b3a7247c17..9fb1a19db9 100644 --- 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 :