Subterminal precategories and constant functors (#941)

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

src/category-theory/constant-functors.lagda.md

@@ -0,0 +1,107 @@
+# Constant functors
+
+```agda
+module category-theory.constant-functors where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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

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

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

src/category-theory/subterminal-precategories.lagda.md

@@ -0,0 +1,67 @@
+# Subterminal precategories
+
+```agda
+module category-theory.subterminal-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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)
+```

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)