Initial and terminal copresheaves (#1174)

Adding initial and terminal copresheaves.

---------

Co-authored-by: Fredrik Bakke <[email protected]>

Author: FernandoChu

src/category-theory/copresheaf-categories.lagda.md

@@ -9,24 +9,32 @@ module category-theory.copresheaf-categories where
 ```agda
 open import category-theory.categories
 open import category-theory.category-of-functors-from-small-to-large-categories
+open import category-theory.constant-functors
 open import category-theory.functors-from-small-to-large-precategories
 open import category-theory.functors-precategories
+open import category-theory.initial-objects-precategories
 open import category-theory.large-categories
 open import category-theory.large-precategories
 open import category-theory.natural-transformations-functors-from-small-to-large-precategories
+open import category-theory.natural-transformations-functors-precategories
 open import category-theory.precategories
 open import category-theory.precategory-of-functors-from-small-to-large-precategories
+open import category-theory.terminal-objects-precategories
 
 open import foundation.category-of-sets
 open import foundation.commuting-squares-of-maps
 open import foundation.dependent-pair-types
+open import foundation.empty-types
 open import foundation.equality-cartesian-product-types
 open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.propositions
+open import foundation.raising-universe-levels
 open import foundation.sets
+open import foundation.unit-type
 open import foundation.universe-levels
 ```
 
@@ -307,6 +315,115 @@ module _
             ( pr2 w)))
 ```
 
+### The initial copresheaf
+
+Since colimits are computed pointwise, the initial copresheaf is the constant
+functor at the empty set.
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2) (l : Level)
+  where
+
+  obj-initial-copresheaf-Precategory :
+    copresheaf-Precategory C l
+  obj-initial-copresheaf-Precategory =
+    constant-functor-Precategory
+      C (Set-Precategory l) (raise-empty-Set l)
+
+  hom-initial-copresheaf-Precategory :
+    ( X : copresheaf-Precategory C l) →
+    hom-Precategory
+      (copresheaf-precategory-Precategory C l)
+      obj-initial-copresheaf-Precategory
+      X
+  pr1 (hom-initial-copresheaf-Precategory X) x (map-raise ())
+  pr2 (hom-initial-copresheaf-Precategory X) f =
+    eq-htpy (λ where (map-raise ()))
+
+  is-unique-hom-initial-copresheaf-Precategory :
+    ( X : copresheaf-Precategory C l) →
+    ( τ :
+      hom-Precategory
+        (copresheaf-precategory-Precategory C l)
+        obj-initial-copresheaf-Precategory
+        X) →
+    hom-initial-copresheaf-Precategory X ＝ τ
+  is-unique-hom-initial-copresheaf-Precategory X τ =
+    eq-htpy-hom-family-natural-transformation-Precategory
+      ( C)
+      ( Set-Precategory l)
+      ( obj-initial-copresheaf-Precategory)
+      ( X)
+      ( hom-initial-copresheaf-Precategory X)
+      ( τ)
+      ( λ x → eq-htpy (λ where (map-raise ())))
+
+  initial-copresheaf-Precategory :
+    initial-obj-Precategory
+      (copresheaf-precategory-Precategory C l)
+  pr1 initial-copresheaf-Precategory =
+    obj-initial-copresheaf-Precategory
+  pr1 (pr2 initial-copresheaf-Precategory X) =
+    hom-initial-copresheaf-Precategory X
+  pr2 (pr2 initial-copresheaf-Precategory X) τ =
+    is-unique-hom-initial-copresheaf-Precategory X τ
+```
+
+### The terminal copresheaf
+
+Since limits are computed pointwise, the terminal copresheaf is the constant
+functor at the terminal set.
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2) (l : Level)
+  where
+
+  obj-terminal-copresheaf-Precategory :
+    copresheaf-Precategory C l
+  obj-terminal-copresheaf-Precategory =
+    constant-functor-Precategory
+      C (Set-Precategory l) (raise-unit-Set l)
+
+  hom-terminal-copresheaf-Precategory :
+    ( X : copresheaf-Precategory C l) →
+    hom-Precategory
+      (copresheaf-precategory-Precategory C l)
+      X
+      obj-terminal-copresheaf-Precategory
+  pr1 (hom-terminal-copresheaf-Precategory X) c m = raise-star
+  pr2 (hom-terminal-copresheaf-Precategory X) f = refl
+
+  is-unique-hom-terminal-copresheaf-Precategory :
+    ( X : copresheaf-Precategory C l) →
+    ( τ :
+      hom-Precategory
+        (copresheaf-precategory-Precategory C l)
+        X
+        obj-terminal-copresheaf-Precategory) →
+    hom-terminal-copresheaf-Precategory X ＝ τ
+  is-unique-hom-terminal-copresheaf-Precategory X τ =
+    eq-htpy-hom-family-natural-transformation-Precategory
+      ( C)
+      ( Set-Precategory l)
+      ( X)
+      ( obj-terminal-copresheaf-Precategory)
+      ( hom-terminal-copresheaf-Precategory X)
+      ( τ)
+      ( λ x → eq-htpy (λ _ → eq-is-prop is-prop-raise-unit))
+
+  terminal-copresheaf-Precategory :
+    terminal-obj-Precategory
+      (copresheaf-precategory-Precategory C l)
+  pr1 terminal-copresheaf-Precategory =
+    obj-terminal-copresheaf-Precategory
+  pr1 (pr2 terminal-copresheaf-Precategory X) =
+    hom-terminal-copresheaf-Precategory X
+  pr2 (pr2 terminal-copresheaf-Precategory X) τ =
+    is-unique-hom-terminal-copresheaf-Precategory X τ
+```
+
 ## See also
 
 - [The Yoneda lemma](category-theory.yoneda-lemma-precategories.md)

src/foundation/empty-types.lagda.md

@@ -22,6 +22,9 @@ open import foundation-core.contractible-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.function-types
 open import foundation-core.propositions
+open import foundation-core.sets
+open import foundation-core.truncated-types
+open import foundation-core.truncation-levels
 ```
 
 </details>
@@ -105,6 +108,8 @@ pr1 (is-nonempty-Prop A) = is-nonempty A
 pr2 (is-nonempty-Prop A) = is-property-is-empty
 ```
 
+### Being empty is preserved under propositional truncations
+
 ```agda
 abstract
   is-empty-type-trunc-Prop :
@@ -128,6 +133,8 @@ abstract
     map-universal-property-trunc-Prop (is-nonempty-Prop X) (λ x f → f x)
 ```
 
+### Properties for the raised empty type
+
 ```agda
 abstract
   is-prop-raise-empty :
@@ -146,6 +153,16 @@ abstract
   is-empty-raise-empty :
     {l1 : Level} → is-empty (raise-empty l1)
   is-empty-raise-empty {l1} = map-inv-equiv (compute-raise-empty l1)
+
+abstract
+  is-set-raise-empty :
+    {l1 : Level} → is-set (raise-empty l1)
+  is-set-raise-empty = is-trunc-succ-is-trunc neg-one-𝕋 is-prop-raise-empty
+
+raise-empty-Set :
+  (l1 : Level) → Set l1
+pr1 (raise-empty-Set l1) = raise-empty l1
+pr2 (raise-empty-Set l1) = is-set-raise-empty
 ```
 
 ### The type of all empty types of a given universe is contractible