Update category theory tables and define category of simplicial sets

src/category-theory.lagda.md

@@ -25,6 +25,7 @@ open import category-theory.category-of-functors public
 open import category-theory.category-of-functors-from-small-to-large-categories public
 open import category-theory.category-of-maps-categories public
 open import category-theory.category-of-maps-from-small-to-large-categories public
+open import category-theory.category-of-simplicial-sets public
 open import category-theory.commuting-squares-of-morphisms-in-large-precategories public
 open import category-theory.commuting-squares-of-morphisms-in-precategories public
 open import category-theory.commuting-squares-of-morphisms-in-set-magmoids public

src/category-theory/category-of-simplicial-sets.lagda.md

@@ -0,0 +1,169 @@
+# The category of simplicial sets
+
+```agda
+module category-theory.category-of-simplicial-sets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.large-categories
+open import category-theory.large-precategories
+open import category-theory.precategories
+open import category-theory.presheaf-categories
+open import category-theory.simplex-category
+
+open import foundation.commuting-squares-of-maps
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.strictly-involutive-identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The {{#concept "large category of simplicial sets" Agda=sSet-Large-Category}} is
+the [presheaf category](category-theory.presheaf-categories.md) on the
+[simplex category](category-theory.simplex-category.md)
+
+```text
+  Δᵒᵖ → Set.
+```
+
+To this large category, there is an associated
+[small category](category-theory.categories.md) of **small simplicial sets**,
+taking values in small [sets](foundation-core.sets.md).
+
+## Definitions
+
+### The large category of simplicial sets
+
+```agda
+sSet-Large-Precategory :
+  Large-Precategory lsuc (_⊔_)
+sSet-Large-Precategory =
+  presheaf-large-precategory-Precategory simplex-Precategory
+
+is-large-category-sSet-Large-Category :
+  is-large-category-Large-Precategory sSet-Large-Precategory
+is-large-category-sSet-Large-Category =
+  is-large-category-presheaf-large-category-Precategory simplex-Precategory
+
+sSet-Large-Category :
+  Large-Category lsuc (_⊔_)
+sSet-Large-Category =
+  presheaf-large-category-Precategory simplex-Precategory
+
+sSet : (l : Level) → UU (lsuc l)
+sSet = obj-Large-Category sSet-Large-Category
+
+module _
+  {l1 : Level} (X : sSet l1)
+  where
+
+  element-set-sSet : obj-simplex-Category → Set l1
+  element-set-sSet = element-set-presheaf-Precategory simplex-Precategory X
+
+  element-sSet : obj-simplex-Category → UU l1
+  element-sSet X = type-Set (element-set-sSet X)
+
+  action-sSet :
+    {X Y : obj-simplex-Category} →
+    hom-simplex-Category X Y → element-sSet Y → element-sSet X
+  action-sSet = action-presheaf-Precategory simplex-Precategory X
+
+  preserves-id-action-sSet :
+    {X : obj-simplex-Category} →
+    action-sSet {X} {X} (id-hom-simplex-Category X) ~ id
+  preserves-id-action-sSet =
+    preserves-id-action-presheaf-Precategory simplex-Precategory X
+
+  preserves-comp-action-sSet :
+    {X Y Z : obj-simplex-Category}
+    (g : hom-simplex-Category Y Z) (f : hom-simplex-Category X Y) →
+    action-sSet (comp-hom-simplex-Category g f) ~
+    action-sSet f ∘ action-sSet g
+  preserves-comp-action-sSet =
+    preserves-comp-action-presheaf-Precategory simplex-Precategory X
+
+hom-set-sSet : {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) → Set (l1 ⊔ l2)
+hom-set-sSet = hom-set-Large-Category sSet-Large-Category
+
+hom-sSet : {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) → UU (l1 ⊔ l2)
+hom-sSet = hom-Large-Category sSet-Large-Category
+
+module _
+  {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) (h : hom-sSet X Y)
+  where
+
+  map-hom-sSet :
+    (F : obj-simplex-Category) → element-sSet X F → element-sSet Y F
+  map-hom-sSet = map-hom-presheaf-Precategory simplex-Precategory X Y h
+
+  naturality-hom-sSet :
+    {F E : obj-simplex-Category} (f : hom-simplex-Category F E) →
+    coherence-square-maps
+      ( action-sSet X f)
+      ( map-hom-sSet E)
+      ( map-hom-sSet F)
+      ( action-sSet Y f)
+  naturality-hom-sSet =
+    naturality-hom-presheaf-Precategory simplex-Precategory X Y h
+
+comp-hom-sSet :
+  {l1 l2 l3 : Level} (X : sSet l1) (Y : sSet l2) (Z : sSet l3) →
+  hom-sSet Y Z → hom-sSet X Y → hom-sSet X Z
+comp-hom-sSet = comp-hom-presheaf-Precategory simplex-Precategory
+
+id-hom-sSet : {l1 : Level} (X : sSet l1) → hom-sSet X X
+id-hom-sSet = id-hom-presheaf-Precategory simplex-Precategory
+
+associative-comp-hom-sSet :
+  {l1 l2 l3 l4 : Level}
+  (X : sSet l1) (Y : sSet l2) (Z : sSet l3) (W : sSet l4)
+  (h : hom-sSet Z W) (g : hom-sSet Y Z) (f : hom-sSet X Y) →
+  comp-hom-sSet X Y W (comp-hom-sSet Y Z W h g) f ＝
+  comp-hom-sSet X Z W h (comp-hom-sSet X Y Z g f)
+associative-comp-hom-sSet =
+  associative-comp-hom-presheaf-Precategory simplex-Precategory
+
+involutive-eq-associative-comp-hom-sSet :
+  {l1 l2 l3 l4 : Level}
+  (X : sSet l1) (Y : sSet l2) (Z : sSet l3) (W : sSet l4)
+  (h : hom-sSet Z W) (g : hom-sSet Y Z) (f : hom-sSet X Y) →
+  comp-hom-sSet X Y W (comp-hom-sSet Y Z W h g) f ＝ⁱ
+  comp-hom-sSet X Z W h (comp-hom-sSet X Y Z g f)
+involutive-eq-associative-comp-hom-sSet =
+  involutive-eq-associative-comp-hom-presheaf-Precategory simplex-Precategory
+
+left-unit-law-comp-hom-sSet :
+  {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) (f : hom-sSet X Y) →
+  comp-hom-sSet X Y Y (id-hom-sSet Y) f ＝ f
+left-unit-law-comp-hom-sSet =
+  left-unit-law-comp-hom-presheaf-Precategory simplex-Precategory
+
+right-unit-law-comp-hom-sSet :
+  {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) (f : hom-sSet X Y) →
+  comp-hom-sSet X X Y f (id-hom-sSet X) ＝ f
+right-unit-law-comp-hom-sSet =
+  right-unit-law-comp-hom-presheaf-Precategory simplex-Precategory
+```
+
+### The category of small simplicial sets
+
+```agda
+sSet-Precategory : (l : Level) → Precategory (lsuc l) l
+sSet-Precategory = precategory-Large-Category sSet-Large-Category
+
+sSet-Category : (l : Level) → Category (lsuc l) l
+sSet-Category = category-Large-Category sSet-Large-Category
+```
+
+## External links
+
+- [simplicial set](https://ncatlab.org/nlab/show/simplicial+set) on $n$Lab

src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md

@@ -217,12 +217,15 @@ module _
 
 ### Being unital is a property of composition operations on binary families of sets
 
-**Proof:** Suppose `e e' : (x : A) → hom-set x x` are both right and left units
-with regard to composition. It is enough to show that `e ＝ e'` since the right
-and left unit laws are propositions (because all hom-types are sets). By
-function extensionality, it is enough to show that `e x ＝ e' x` for all
-`x : A`. But by the unit laws we have the following chain of equalities:
-`e x ＝ (e' x) ∘ (e x) ＝ e' x.`
+**Proof:** Suppose `e e' : (x : A) → hom x x` are both two-sided units with
+respect to composition. It is enough to show that `e ＝ e'` since the right and
+left unit laws are propositions by the set-condition on hom-types. By function
+extensionality, it is enough to show that `e x ＝ e' x` for all `x : A`, and by
+the unit laws we have:
+
+```text
+  e x ＝ (e' x) ∘ (e x) ＝ e' x. ∎
+```
 
 ```agda
 module _

src/category-theory/set-magmoids.lagda.md

@@ -22,18 +22,20 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **set-magmoid** is the [structure](foundation.structure.md) of a
+A {{#concept "set-magmoid" Agda=Set-Magmoid}} is the
+[structure](foundation.structure.md) of a
 [composition operation on a binary family of sets](category-theory.composition-operations-on-binary-families-of-sets.md),
-and are in one sense the "oidification" of [magmas](structured-types.magmas.md)
-in [sets](foundation-core.sets.md). We call elements of the indexing type
-**objects**, and elements of the set-family **morphisms** or **homomorphisms**.
+and are the _oidification_ of [magmas](structured-types.magmas.md) in
+[sets](foundation-core.sets.md) in one sense of the term. We call elements of
+the indexing type **objects**, and elements of the set-family **morphisms** or
+**homomorphisms**.
 
-These objects serve as our starting point in the study of the
+Set-magmoids serve as our starting point in the study of the
 [structure](foundation.structure.md) of
 [categories](category-theory.categories.md). Indeed, categories form a
 [subtype](foundation-core.subtypes.md) of set-magmoids, although
-structure-preserving maps of set-magmoids do not automatically preserve
-identity-morphisms.
+structure-preserving maps of set-magmoids do not automatically preserve identity
+morphisms.
 
 Set-magmoids are commonly referred to as _magmoids_ in the literature, but we
 use the "set-" prefix to make clear its relation to magmas. Set-magmoids should
@@ -152,12 +154,15 @@ module _
 ### The predicate on set-magmoids of being unital
 
 **Proof:** To show that unitality is a proposition, suppose
-`e e' : (x : A) → hom-set x x` are both right and left units with regard to
-composition. It is enough to show that `e ＝ e'` since the right and left unit
-laws are propositions (because all hom-types are sets). By function
-extensionality, it is enough to show that `e x ＝ e' x` for all `x : A`. But by
-the unit laws we have the following chain of equalities:
-`e x ＝ (e' x) ∘ (e x) ＝ e' x.`
+`e e' : (x : A) → hom x x` are both two-sided units with respect to composition.
+It is enough to show that `e ＝ e'` since the right and left unit laws are
+propositions by the set-condition on hom-types. By function extensionality, it
+is enough to show that `e x ＝ e' x` for all `x : A`, and by the unit laws we
+have:
+
+```text
+  e x ＝ (e' x) ∘ (e x) ＝ e' x. ∎
+```
 
 ```agda
 module _
@@ -218,6 +223,8 @@ module _
 
 ## See also
 
+- [Magmas](structured-types.magmas.md) are types equipped with a binary
+  operation.
 - [Nonunital precategories](category-theory.nonunital-precategories.md) are
   associative set-magmoids.
 - [Precategories](category-theory.precategories.md) are associative and unital

tables/categories.md

@@ -1,13 +1,23 @@
-| Category                          | File                                                                                                                                          |
-| --------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- |
-| Abelian groups                    | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md)                                                       |
-| Commutative Rings                 | [`commutative-algebra.category-of-commutative-rings`](commutative-algebra.category-of-commutative-rings.md)                                   |
-| Connected set bundles over 𝕊¹     | [`synthetic-homotopy-theory.category-of-connected-set-bundles-circle`](synthetic-homotopy-theory.category-of-connected-set-bundles-circle.md) |
-| Families of sets                  | [`foundation.category-of-families-of-sets`](foundation.category-of-families-of-sets.md)                                                       |
-| Groups                            | [`group-theory.category-of-groups`](group-theory.category-of-groups.md)                                                                       |
-| `G`-sets                          | [`group-theory.category-of-group-actions`](group-theory.category-of-group-actions.md)                                                         |
-| Metric spaces and isometries      | [`metric-spaces.category-of-metric-spaces-and-isometries`](metric-spaces.category-of-metric-spaces-and-isometries.md)                         |
-| Metric spaces and short functions | [`metric-spaces.category-of-metric-spaces-and-short-functions`](metric-spaces.category-of-metric-spaces-and-short-functions.md)               |
-| Rings                             | [`ring-theory.category-of-rings`](ring-theory.category-of-rings.md)                                                                           |
-| Semigroups                        | [`group-theory.category-of-semigroups`](group-theory.category-of-semigroups.md)                                                               |
-| Sets                              | [`foundation.category-of-sets`](foundation.category-of-sets.md)                                                                               |
+| Category                          | File                                                                                                                                                                                                                                    |
+| --------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
+| Abelian groups                    | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md)                                                                                                                                                 |
+| Augmented simplex category        | [`category-theory.augmented-simplex-category`](category-theory.augmented-simplex-category.md)                                                                                                                                           |
+| Commutative rings                 | [`commutative-algebra.category-of-commutative-rings`](commutative-algebra.category-of-commutative-rings.md)                                                                                                                             |
+| Connected set bundles over 𝕊¹     | [`synthetic-homotopy-theory.category-of-connected-set-bundles-circle`](synthetic-homotopy-theory.category-of-connected-set-bundles-circle.md)                                                                                           |
+| Copresheaves on a precategory     | [`category-theory.copresheaf-categories`](category-theory.copresheaf-categories.md)                                                                                                                                                     |
+| Cyclic rings                      | [`ring-theory.category-of-cyclic-rings`](ring-theory.category-of-cyclic-rings.md)                                                                                                                                                       |
+| Functors between two categories   | [`category-theory.category-of-functors`](category-theory.category-of-functors.md) [`category-theory.category-of-functors-from-small-to-large-categories`](category-theory.category-of-functors-from-small-to-large-categories.md)       |
+| Families of sets                  | [`foundation.category-of-families-of-sets`](foundation.category-of-families-of-sets.md)                                                                                                                                                 |
+| Groups                            | [`group-theory.category-of-groups`](group-theory.category-of-groups.md)                                                                                                                                                                 |
+| `G`-sets                          | [`group-theory.category-of-group-actions`](group-theory.category-of-group-actions.md)                                                                                                                                                   |
+| Maps between two categories       | [`category-theory.category-of-maps-categories`](category-theory.category-of-maps-categories.md) [`category-theory.category-of-maps-from-small-to-large-categories`](category-theory.category-of-maps-from-small-to-large-categories.md) |
+| Metric spaces and isometries      | [`metric-spaces.category-of-metric-spaces-and-isometries`](metric-spaces.category-of-metric-spaces-and-isometries.md)                                                                                                                   |
+| Metric spaces and short functions | [`metric-spaces.category-of-metric-spaces-and-short-functions`](metric-spaces.category-of-metric-spaces-and-short-functions.md)                                                                                                         |
+| Orbits of a group                 | [`group-theory.category-of-orbits-groups`](group-theory.category-of-orbits-groups.md)                                                                                                                                                   |
+| Presheaves on a precategory       | [`category-theory.presheaf-categories`](category-theory.presheaf-categories.md)                                                                                                                                                         |
+| Representing arrow category       | [`category-theory.representing-arrow-category`](category-theory.representing-arrow-category.md)                                                                                                                                         |
+| Rings                             | [`ring-theory.category-of-rings`](ring-theory.category-of-rings.md)                                                                                                                                                                     |
+| Semigroups                        | [`group-theory.category-of-semigroups`](group-theory.category-of-semigroups.md)                                                                                                                                                         |
+| Sets                              | [`foundation.category-of-sets`](foundation.category-of-sets.md)                                                                                                                                                                         |
+| Simplex category                  | [`category-theory.simplex-category`](category-theory.simplex-category.md)                                                                                                                                                               |
+| Simplicial sets                   | [`category-theory.category-of-simplicial-sets`](category-theory.category-of-simplicial-sets.md)                                                                                                                                         |