From 5c6eadfd198c54facd84c0e8f2363bcf920df680 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 24 Nov 2023 23:01:46 +0100 Subject: [PATCH] Subterminal precategories and constant functors (#941) --- src/category-theory.lagda.md | 2 + .../constant-functors.lagda.md | 107 ++++++++++++++++++ .../indiscrete-precategories.lagda.md | 19 ++-- src/category-theory/initial-category.lagda.md | 13 ++- .../subterminal-precategories.lagda.md | 67 +++++++++++ .../terminal-category.lagda.md | 36 +++--- .../truncation-equivalences.lagda.md | 18 +-- 7 files changed, 221 insertions(+), 41 deletions(-) create mode 100644 src/category-theory/constant-functors.lagda.md create mode 100644 src/category-theory/subterminal-precategories.lagda.md diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 0d7669aa8d..4e63136520 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -28,6 +28,7 @@ open import category-theory.commuting-squares-of-morphisms-in-precategories publ open import category-theory.commuting-squares-of-morphisms-in-set-magmoids public open import category-theory.composition-operations-on-binary-families-of-sets public open import category-theory.conservative-functors-precategories public +open import category-theory.constant-functors public open import category-theory.copresheaf-categories public open import category-theory.coproducts-in-precategories public open import category-theory.cores-categories public @@ -145,6 +146,7 @@ open import category-theory.strict-categories public open import category-theory.structure-equivalences-set-magmoids public open import category-theory.subcategories public open import category-theory.subprecategories public +open import category-theory.subterminal-precategories public open import category-theory.terminal-category public open import category-theory.terminal-objects-precategories public open import category-theory.wide-subcategories public diff --git a/src/category-theory/constant-functors.lagda.md b/src/category-theory/constant-functors.lagda.md new file mode 100644 index 0000000000..993305ddcb --- /dev/null +++ b/src/category-theory/constant-functors.lagda.md @@ -0,0 +1,107 @@ +# Constant functors + +```agda +module category-theory.constant-functors where +``` + +
Imports + +```agda +open import category-theory.categories +open import category-theory.functors-categories +open import category-theory.functors-large-categories +open import category-theory.functors-large-precategories +open import category-theory.functors-precategories +open import category-theory.large-categories +open import category-theory.large-precategories +open import category-theory.precategories + +open import foundation.dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +A **constant functor** is a [functor](category-theory.functors-categories.md) +`F : C → D` that is constant at an object `d ∈ D` and the identity morphism at +that object. + +## Definition + +### Constant functors between precategories + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) + (d : obj-Precategory D) + where + + constant-functor-Precategory : functor-Precategory C D + pr1 constant-functor-Precategory _ = d + pr1 (pr2 constant-functor-Precategory) _ = id-hom-Precategory D + pr1 (pr2 (pr2 constant-functor-Precategory)) _ _ = + inv (left-unit-law-comp-hom-Precategory D (id-hom-Precategory D)) + pr2 (pr2 (pr2 constant-functor-Precategory)) = refl-htpy +``` + +### Constant functors between categories + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Category l1 l2) (D : Category l3 l4) + (d : obj-Category D) + where + + constant-functor-Category : functor-Category C D + constant-functor-Category = + constant-functor-Precategory + ( precategory-Category C) + ( precategory-Category D) + ( d) +``` + +### Constant functors between large precategories + +```agda +module _ + {αC αD : Level → Level} {βC βD : Level → Level → Level} + (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) + {l : Level} (d : obj-Large-Precategory D l) + where + + constant-functor-Large-Precategory : functor-Large-Precategory (λ _ → l) C D + obj-functor-Large-Precategory constant-functor-Large-Precategory _ = d + hom-functor-Large-Precategory constant-functor-Large-Precategory _ = + id-hom-Large-Precategory D + preserves-comp-functor-Large-Precategory constant-functor-Large-Precategory + _ _ = + inv + ( left-unit-law-comp-hom-Large-Precategory D (id-hom-Large-Precategory D)) + preserves-id-functor-Large-Precategory constant-functor-Large-Precategory = + refl +``` + +### Constant functors between large categories + +```agda +module _ + {αC αD : Level → Level} {βC βD : Level → Level → Level} + (C : Large-Category αC βC) (D : Large-Category αD βD) + {l : Level} (d : obj-Large-Category D l) + where + + constant-functor-Large-Category : functor-Large-Category (λ _ → l) C D + constant-functor-Large-Category = + constant-functor-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( d) +``` + +## External links + +- [constant functor](https://ncatlab.org/nlab/show/constant+functor) at $n$Lab diff --git a/src/category-theory/indiscrete-precategories.lagda.md b/src/category-theory/indiscrete-precategories.lagda.md index 7f7dfeaed5..8620c48f27 100644 --- a/src/category-theory/indiscrete-precategories.lagda.md +++ b/src/category-theory/indiscrete-precategories.lagda.md @@ -14,6 +14,7 @@ open import category-theory.precategories open import category-theory.pregroupoids open import category-theory.preunivalent-categories open import category-theory.strict-categories +open import category-theory.subterminal-precategories open import category-theory.terminal-category open import foundation.action-on-identifications-functions @@ -44,7 +45,8 @@ hom-[sets](foundation-core.sets.md) are This construction demonstrates one essential aspect about precategories: While it displays `obj-Precategory` as a [retraction](foundation-core.retractions.md), -up to weak categorical equivalence, every indiscrete precategory is subterminal. +every indiscrete precategory is +[subterminal](category-theory.subterminal-precategories.md). ## Definitions @@ -217,6 +219,10 @@ module _ ### If an indiscrete precategory is preunivalent then it is a strict category +**Proof:** If an indiscrete precategory is preunivalent, that means every +identity type of the objects embeds into the unit type, hence the objects form a +set. + ```agda module _ {l : Level} (X : UU l) @@ -242,19 +248,16 @@ is-section-indiscrete-Precategory : is-section-indiscrete-Precategory X = refl ``` -### The terminal projection functor is fully faithful +### Indiscrete precategories are subterminal ```agda module _ {l : Level} (X : UU l) where - is-fully-faithful-terminal-functor-indiscrete-Precategory : - is-fully-faithful-functor-Precategory - ( indiscrete-Precategory X) - ( terminal-Precategory) - ( terminal-functor-Precategory (indiscrete-Precategory X)) - is-fully-faithful-terminal-functor-indiscrete-Precategory x y = is-equiv-id + is-subterminal-indiscrete-Precategory : + is-subterminal-Precategory (indiscrete-Precategory X) + is-subterminal-indiscrete-Precategory x y = is-equiv-id ``` ## External links diff --git a/src/category-theory/initial-category.lagda.md b/src/category-theory/initial-category.lagda.md index 6633eba1cc..b0976ba941 100644 --- a/src/category-theory/initial-category.lagda.md +++ b/src/category-theory/initial-category.lagda.md @@ -149,12 +149,13 @@ module _ ( F) ( (λ where ()) , (λ where {()})) - is-contr-functor-initial-Precategory : - is-contr (functor-Precategory initial-Precategory C) - pr1 is-contr-functor-initial-Precategory = - initial-functor-Precategory - pr2 is-contr-functor-initial-Precategory = - uniqueness-initial-functor-Precategory + abstract + is-contr-functor-initial-Precategory : + is-contr (functor-Precategory initial-Precategory C) + pr1 is-contr-functor-initial-Precategory = + initial-functor-Precategory + pr2 is-contr-functor-initial-Precategory = + uniqueness-initial-functor-Precategory ``` ## See also diff --git a/src/category-theory/subterminal-precategories.lagda.md b/src/category-theory/subterminal-precategories.lagda.md new file mode 100644 index 0000000000..124025252f --- /dev/null +++ b/src/category-theory/subterminal-precategories.lagda.md @@ -0,0 +1,67 @@ +# Subterminal precategories + +```agda +module category-theory.subterminal-precategories where +``` + +
Imports + +```agda +open import category-theory.composition-operations-on-binary-families-of-sets +open import category-theory.fully-faithful-functors-precategories +open import category-theory.isomorphisms-in-precategories +open import category-theory.precategories +open import category-theory.pregroupoids +open import category-theory.preunivalent-categories +open import category-theory.strict-categories +open import category-theory.terminal-category + +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.iterated-dependent-product-types +open import foundation.propositions +open import foundation.sets +open import foundation.subtype-identity-principle +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +A [precategory](category-theory.precategories.md) is **subterminal** if its +[terminal projection functor](category-theory.terminal-category.md) is +[fully faithful](category-theory.fully-faithful-functors-precategories.md). + +## Definitions + +### The predicate of being subterminal on precategories + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + is-subterminal-Precategory : UU (l1 ⊔ l2) + is-subterminal-Precategory = + is-fully-faithful-functor-Precategory C terminal-Precategory + ( terminal-functor-Precategory C) + + is-subterminal-prop-Precategory : Prop (l1 ⊔ l2) + is-subterminal-prop-Precategory = + is-fully-faithful-prop-functor-Precategory C terminal-Precategory + ( terminal-functor-Precategory C) + + is-prop-is-subterminal-Precategory : is-prop is-subterminal-Precategory + is-prop-is-subterminal-Precategory = + is-prop-is-fully-faithful-functor-Precategory C terminal-Precategory + ( terminal-functor-Precategory C) +``` diff --git a/src/category-theory/terminal-category.lagda.md b/src/category-theory/terminal-category.lagda.md index 8fa88bd729..51418bcab2 100644 --- a/src/category-theory/terminal-category.lagda.md +++ b/src/category-theory/terminal-category.lagda.md @@ -9,6 +9,8 @@ module category-theory.terminal-category where ```agda open import category-theory.categories open import category-theory.composition-operations-on-binary-families-of-sets +open import category-theory.constant-functors +open import category-theory.functors-categories open import category-theory.functors-precategories open import category-theory.gaunt-categories open import category-theory.isomorphisms-in-categories @@ -172,23 +174,23 @@ pr1 terminal-Gaunt-Category = terminal-Category pr2 terminal-Gaunt-Category = is-gaunt-terminal-Category ``` -### Points in a precategory +### Points in categories Using the terminal category as the representing category of objects, we can define, given an object in a category `x ∈ C`, the _point_ at `x` as the -constant functor from the terminal category to `C` at `x`. +[constant functor](category-theory.constant-functors.md) from the terminal +category to `C` at `x`. ```agda -module _ - {l1 l2 : Level} (C : Precategory l1 l2) (x : obj-Precategory C) - where - - point-Precategory : functor-Precategory terminal-Precategory C - pr1 point-Precategory _ = x - pr1 (pr2 point-Precategory) _ = id-hom-Precategory C - pr1 (pr2 (pr2 point-Precategory)) _ _ = - inv (left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)) - pr2 (pr2 (pr2 point-Precategory)) _ = refl +point-Precategory : + {l1 l2 : Level} (C : Precategory l1 l2) (x : obj-Precategory C) → + functor-Precategory terminal-Precategory C +point-Precategory = constant-functor-Precategory terminal-Precategory + +point-Category : + {l1 l2 : Level} (C : Category l1 l2) (x : obj-Category C) → + functor-Category terminal-Category C +point-Category C = point-Precategory (precategory-Category C) ``` ## Properties @@ -206,7 +208,7 @@ module _ ( λ F → obj-functor-Precategory terminal-Precategory C F star) ( λ F → eq-htpy-functor-Precategory terminal-Precategory C _ F - ( refl-htpy , + ( ( refl-htpy) , ( λ _ → ap ( λ f → comp-hom-Precategory C f (id-hom-Precategory C)) @@ -234,10 +236,8 @@ module _ where terminal-functor-Precategory : functor-Precategory C terminal-Precategory - pr1 terminal-functor-Precategory _ = star - pr1 (pr2 terminal-functor-Precategory) _ = star - pr1 (pr2 (pr2 terminal-functor-Precategory)) _ _ = refl - pr2 (pr2 (pr2 terminal-functor-Precategory)) _ = refl + terminal-functor-Precategory = + constant-functor-Precategory C terminal-Precategory star uniqueness-terminal-functor-Precategory : (F : functor-Precategory C terminal-Precategory) → @@ -248,7 +248,7 @@ module _ ( terminal-Precategory) ( terminal-functor-Precategory) ( F) - ((λ _ → refl) , (λ _ → refl)) + ( refl-htpy , refl-htpy) is-contr-functor-terminal-Precategory : is-contr (functor-Precategory C terminal-Precategory) diff --git a/src/foundation/truncation-equivalences.lagda.md b/src/foundation/truncation-equivalences.lagda.md index 2965e48bc9..ee2ac19812 100644 --- a/src/foundation/truncation-equivalences.lagda.md +++ b/src/foundation/truncation-equivalences.lagda.md @@ -262,7 +262,7 @@ module _ ### The map on dependent pair types induced by the unit of the `(k+1)`-truncation is a `k`-equivalence This is an instance of Lemma 2.27 in Christensen, Opie, Rijke & Scoccola -[CORS'20] listed below. +\[CORS'20\] listed below. ```agda module _ @@ -294,7 +294,7 @@ module _ ### There is an `k`-equivalence between the fiber of a map and the fiber of its `(k+1)`-truncation -This is an instance of Corollary 2.29 in [CORS'20]. +This is an instance of Corollary 2.29 in \[CORS'20\]. We consider the following composition of maps @@ -380,7 +380,7 @@ module _ ### Every `(k+1)`-equivalence is `k`-connected -This is an instance of Proposition 2.30 in [CORS'20]. +This is an instance of Proposition 2.30 in \[CORS'20\]. ```agda module _ @@ -397,7 +397,7 @@ module _ ### The codomain of a `k`-connected map is `(k+1)`-connected if its domain is `(k+1)`-connected -This follows part of the proof of Proposition 2.31 in [CORS'20]. +This follows part of the proof of Proposition 2.31 in \[CORS'20\]. ```agda module _ @@ -448,7 +448,7 @@ module _ ### If `g ∘ f` is `(k+1)`-connected, then `f` is `k`-connected if and only if `g` is `(k+1)`-connected -This is an instance of Proposition 2.31 in [CORS'20]. +This is an instance of Proposition 2.31 in \[CORS'20\]. ```agda module _ @@ -505,11 +505,11 @@ The notion of `k`-equivalence is a special case of the notion of `L`-equivalence, where `L` is a reflective subuniverse. They were studied in the paper -- J. D. Christensen, M. Opie, E. Rijke, and L. Scoccola. Localization in - Homotopy Type Theory. Higher Structures, 2020. [CORS'20] +- \[CORS'20\]: J. D. Christensen, M. Opie, E. Rijke, and L. Scoccola. + Localization in Homotopy Type Theory. Higher Structures, 2020. The class of `k`-equivalences is left orthogonal to the class of `k`-étale maps. This was shown in -- F. Cherubini, and E. Rijke. Modal descent. Mathematical Structures in Computer - Science, 2021. +- \[CR'21\]: F. Cherubini, and E. Rijke. Modal descent. Mathematical Structures + in Computer Science, 2021.