From a82cb40780888d8c8e5e10027c24734a00be8ad1 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 5 Jun 2025 01:37:57 +0100 Subject: [PATCH 1/7] update tables --- tables/categories.md | 35 ++++++++++++++++++++++------------- tables/precategories.md | 38 +++++++++++++++++--------------------- 2 files changed, 39 insertions(+), 34 deletions(-) diff --git a/tables/categories.md b/tables/categories.md index 36d52caf02..80592a99c3 100644 --- a/tables/categories.md +++ b/tables/categories.md @@ -1,13 +1,22 @@ -| 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 | [`foundation.copresheaf-categories`](foundation.copresheaf-categories.md) | +| Cyclic rings | [`commutative-algebra.category-of-cyclic-rings`](commutative-algebra.category-of-cyclic-rings.md) | +| Functors between two categories | [`foundation.category-of-functors`](foundation.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 | [`foundation.category-of-maps-categories`](foundation.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 | [`foundation.presheaf-categories`](foundation.presheaf-categories.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) | +| Representing arrow category | [`category-theory.representing-arrow-category`](category-theory.representing-arrow-category.md) | diff --git a/tables/precategories.md b/tables/precategories.md index 12c7fd2edf..9851387efc 100644 --- a/tables/precategories.md +++ b/tables/precategories.md @@ -1,21 +1,17 @@ -| Precategory | File | -| --------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------- | -| Abelian groups | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md) | -| Commutative monoids | [`group-theory.precategory-of-commutative-monoids`](group-theory.precategory-of-commutative-monoids.md) | -| Commutative rings | [`commutative-algebra.precategory-of-commutative-rings`](commutative-algebra.precategory-of-commutative-rings.md) | -| Commutative semirings | [`commutative-algebra.precategory-of-commutative-semirings`](commutative-algebra.precategory-of-commutative-semirings.md) | -| Concrete groups | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md) | -| Decidable total orders | [`order-theory.precategory-of-decidable-total-orders`](order-theory.precategory-of-decidable-total-orders.md) | -| Finite species | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md) | -| `G`-sets | [`group-theory.precategory-of-group-actions`](group-theory.precategory-of-group-actions.md) | -| Groups | [`group-theory.precategory-of-groups`](group-theory.precategory-of-groups.md) | -| Metric spaces and functions | [`metric-spaces.precategory-of-metric-spaces-and-functions`](metric-spaces.precategory-of-metric-spaces-and-functions.md) | -| Metric spaces and isometries | [`metric-spaces.precategory-of-metric-spaces-and-isometries`](metric-spaces.precategory-of-metric-spaces-and-isometries.md) | -| Metric spaces and short functions | [`metric-spaces.precategory-of-metric-spaces-and-short-functions`](metric-spaces.precategory-of-metric-spaces-and-short-functions.md) | -| Monoids | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md) | -| Posets | [`order-theory.precategory-of-posets`](order-theory.precategory-of-posets.md) | -| Rings | [`ring-theory.precategory-of-rings`](ring-theory.precategory-of-rings.md) | -| Semigroups | [`group-theory.precategory-of-semigroups`](group-theory.precategory-of-semigroups.md) | -| Semirings | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md) | -| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | -| Total orders | [`order-theory.precategory-of-total-orders`](order-theory.precategory-of-total-orders.md) | +| Precategory | File | +| ----------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------- | +| Algebras of a monad on a precategory | [`category-theory.precategory-of-algebras-monads-precategories`](category-theory.precategory-of-algebras-monads-precategories.md) | +| Commutative monoids | [`group-theory.precategory-of-commutative-monoids`](group-theory.precategory-of-commutative-monoids.md) | +| Commutative rings | [`commutative-algebra.precategory-of-commutative-rings`](commutative-algebra.precategory-of-commutative-rings.md) | +| Commutative semirings | [`commutative-algebra.precategory-of-commutative-semirings`](commutative-algebra.precategory-of-commutative-semirings.md) | +| Concrete groups | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md) | +| Decidable total orders | [`order-theory.precategory-of-decidable-total-orders`](order-theory.precategory-of-decidable-total-orders.md) | +| Finite posets | [`order-theory.precategory-of-finite-posets`](order-theory.precategory-of-finite-posets.md) | +| Finite species | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md) | +| Free algebras of a monad on a precategory | [`category-theory.precategory-of-free-algebras-monads-precategories`](category-theory.precategory-of-free-algebras-monads-precategories.md) | +| Monoids | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md) | +| Orbits of a monoid action | [`group-theory.precategory-of-orbits-monoid-actions`](group-theory.precategory-of-orbits-monoid-actions.md) | +| Posets | [`order-theory.precategory-of-posets`](order-theory.precategory-of-posets.md) | +| Semirings | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md) | +| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | +| Total orders | [`order-theory.precategory-of-total-orders`](order-theory.precategory-of-total-orders.md) | From 656d3123a0987def4003b5c3f1003ccac50a6aee Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 5 Jun 2025 02:08:24 +0100 Subject: [PATCH 2/7] define category of simplicial sets --- src/category-theory.lagda.md | 1 + .../category-of-simplicial-sets.lagda.md | 172 ++++++++++++++++++ tables/categories.md | 1 + 3 files changed, 174 insertions(+) create mode 100644 src/category-theory/category-of-simplicial-sets.lagda.md diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 4e78e73234..fdcd9c6cd7 100644 --- a/src/category-theory.lagda.md +++ b/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 diff --git a/src/category-theory/category-of-simplicial-sets.lagda.md b/src/category-theory/category-of-simplicial-sets.lagda.md new file mode 100644 index 0000000000..3cc5156892 --- /dev/null +++ b/src/category-theory/category-of-simplicial-sets.lagda.md @@ -0,0 +1,172 @@ +# The category of simplicial sets + +```agda +module category-theory.category-of-simplicial-sets where +``` + +
Imports + +```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 +``` + +
+ +## 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} (P : sSet l1) + where + + element-set-sSet : obj-simplex-Category โ†’ Set l1 + element-set-sSet = element-set-presheaf-Precategory simplex-Precategory P + + 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 P + + 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 P + + 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 P + +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} + (P : sSet l1) (Q : sSet l2) + (h : hom-sSet P Q) + where + + map-hom-sSet : + (X : obj-simplex-Category) โ†’ element-sSet P X โ†’ element-sSet Q X + map-hom-sSet = map-hom-presheaf-Precategory simplex-Precategory P Q h + + naturality-hom-sSet : + {X Y : obj-simplex-Category} (f : hom-simplex-Category X Y) โ†’ + coherence-square-maps + ( action-sSet P f) + ( map-hom-sSet Y) + ( map-hom-sSet X) + ( action-sSet Q f) + naturality-hom-sSet = + naturality-hom-presheaf-Precategory simplex-Precategory P Q 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 diff --git a/tables/categories.md b/tables/categories.md index 80592a99c3..85e60ca4bc 100644 --- a/tables/categories.md +++ b/tables/categories.md @@ -19,4 +19,5 @@ | 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) | | Representing arrow category | [`category-theory.representing-arrow-category`](category-theory.representing-arrow-category.md) | From e5cf678fd8eae3984f083310b5c6ad7711b97607 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 5 Jun 2025 02:10:51 +0100 Subject: [PATCH 3/7] sort --- tables/categories.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tables/categories.md b/tables/categories.md index 85e60ca4bc..b8424021a5 100644 --- a/tables/categories.md +++ b/tables/categories.md @@ -15,9 +15,9 @@ | 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 | [`foundation.presheaf-categories`](foundation.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) | -| Representing arrow category | [`category-theory.representing-arrow-category`](category-theory.representing-arrow-category.md) | From 24c11a8c92fedaab8a5a66c29076132e16516c4f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 5 Jun 2025 12:00:35 +0100 Subject: [PATCH 4/7] fix links --- tables/categories.md | 46 ++++++++++++++++++++--------------------- tables/precategories.md | 34 +++++++++++++++--------------- 2 files changed, 40 insertions(+), 40 deletions(-) diff --git a/tables/categories.md b/tables/categories.md index b8424021a5..54b3136228 100644 --- a/tables/categories.md +++ b/tables/categories.md @@ -1,23 +1,23 @@ -| 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 | [`foundation.copresheaf-categories`](foundation.copresheaf-categories.md) | -| Cyclic rings | [`commutative-algebra.category-of-cyclic-rings`](commutative-algebra.category-of-cyclic-rings.md) | -| Functors between two categories | [`foundation.category-of-functors`](foundation.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 | [`foundation.category-of-maps-categories`](foundation.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 | [`foundation.presheaf-categories`](foundation.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) | +| 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) | diff --git a/tables/precategories.md b/tables/precategories.md index 9851387efc..b14b8f58e3 100644 --- a/tables/precategories.md +++ b/tables/precategories.md @@ -1,17 +1,17 @@ -| Precategory | File | -| ----------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------- | -| Algebras of a monad on a precategory | [`category-theory.precategory-of-algebras-monads-precategories`](category-theory.precategory-of-algebras-monads-precategories.md) | -| Commutative monoids | [`group-theory.precategory-of-commutative-monoids`](group-theory.precategory-of-commutative-monoids.md) | -| Commutative rings | [`commutative-algebra.precategory-of-commutative-rings`](commutative-algebra.precategory-of-commutative-rings.md) | -| Commutative semirings | [`commutative-algebra.precategory-of-commutative-semirings`](commutative-algebra.precategory-of-commutative-semirings.md) | -| Concrete groups | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md) | -| Decidable total orders | [`order-theory.precategory-of-decidable-total-orders`](order-theory.precategory-of-decidable-total-orders.md) | -| Finite posets | [`order-theory.precategory-of-finite-posets`](order-theory.precategory-of-finite-posets.md) | -| Finite species | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md) | -| Free algebras of a monad on a precategory | [`category-theory.precategory-of-free-algebras-monads-precategories`](category-theory.precategory-of-free-algebras-monads-precategories.md) | -| Monoids | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md) | -| Orbits of a monoid action | [`group-theory.precategory-of-orbits-monoid-actions`](group-theory.precategory-of-orbits-monoid-actions.md) | -| Posets | [`order-theory.precategory-of-posets`](order-theory.precategory-of-posets.md) | -| Semirings | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md) | -| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | -| Total orders | [`order-theory.precategory-of-total-orders`](order-theory.precategory-of-total-orders.md) | +| Precategory | File | +| ----------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------- | +| Algebras of a monad on a precategory | [`category-theory.precategory-of-algebras-monads-on-precategories`](category-theory.precategory-of-algebras-monads-on-precategories.md) | +| Commutative monoids | [`group-theory.precategory-of-commutative-monoids`](group-theory.precategory-of-commutative-monoids.md) | +| Commutative rings | [`commutative-algebra.precategory-of-commutative-rings`](commutative-algebra.precategory-of-commutative-rings.md) | +| Commutative semirings | [`commutative-algebra.precategory-of-commutative-semirings`](commutative-algebra.precategory-of-commutative-semirings.md) | +| Concrete groups | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md) | +| Decidable total orders | [`order-theory.precategory-of-decidable-total-orders`](order-theory.precategory-of-decidable-total-orders.md) | +| Finite posets | [`order-theory.precategory-of-finite-posets`](order-theory.precategory-of-finite-posets.md) | +| Finite species | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md) | +| Free algebras of a monad on a precategory | [`category-theory.precategory-of-free-algebras-monads-on-precategories`](category-theory.precategory-of-free-algebras-monads-on-precategories.md) | +| Monoids | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md) | +| Orbits of a monoid action | [`group-theory.precategory-of-orbits-monoid-actions`](group-theory.precategory-of-orbits-monoid-actions.md) | +| Posets | [`order-theory.precategory-of-posets`](order-theory.precategory-of-posets.md) | +| Semirings | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md) | +| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | +| Total orders | [`order-theory.precategory-of-total-orders`](order-theory.precategory-of-total-orders.md) | From 3da7993f58ba2c060f3c4264958ffe9c9e695581 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 5 Jun 2025 12:01:15 +0100 Subject: [PATCH 5/7] . --- src/category-theory/category-of-simplicial-sets.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/category-theory/category-of-simplicial-sets.lagda.md b/src/category-theory/category-of-simplicial-sets.lagda.md index 3cc5156892..d1695905b9 100644 --- a/src/category-theory/category-of-simplicial-sets.lagda.md +++ b/src/category-theory/category-of-simplicial-sets.lagda.md @@ -37,7 +37,7 @@ the [presheaf category](category-theory.presheaf-categories.md) on the 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). +taking values in small [sets](foundation-core.sets.md). ## Definitions From af611d13bb3eba8591626433a75a53c9a320b5fd Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 5 Jun 2025 12:05:36 +0100 Subject: [PATCH 6/7] naming --- .../category-of-simplicial-sets.lagda.md | 33 +++++++++---------- 1 file changed, 15 insertions(+), 18 deletions(-) diff --git a/src/category-theory/category-of-simplicial-sets.lagda.md b/src/category-theory/category-of-simplicial-sets.lagda.md index d1695905b9..6797000786 100644 --- a/src/category-theory/category-of-simplicial-sets.lagda.md +++ b/src/category-theory/category-of-simplicial-sets.lagda.md @@ -60,15 +60,14 @@ sSet-Large-Category = presheaf-large-category-Precategory simplex-Precategory sSet : (l : Level) โ†’ UU (lsuc l) -sSet = - obj-Large-Category sSet-Large-Category +sSet = obj-Large-Category sSet-Large-Category module _ - {l1 : Level} (P : sSet l1) + {l1 : Level} (X : sSet l1) where element-set-sSet : obj-simplex-Category โ†’ Set l1 - element-set-sSet = element-set-presheaf-Precategory simplex-Precategory P + 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) @@ -76,13 +75,13 @@ module _ 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 P + 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 P + preserves-id-action-presheaf-Precategory simplex-Precategory X preserves-comp-action-sSet : {X Y Z : obj-simplex-Category} @@ -90,7 +89,7 @@ module _ 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 P + 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 @@ -99,24 +98,22 @@ 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} - (P : sSet l1) (Q : sSet l2) - (h : hom-sSet P Q) + {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) (h : hom-sSet X Y) where map-hom-sSet : - (X : obj-simplex-Category) โ†’ element-sSet P X โ†’ element-sSet Q X - map-hom-sSet = map-hom-presheaf-Precategory simplex-Precategory P Q h + (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 : - {X Y : obj-simplex-Category} (f : hom-simplex-Category X Y) โ†’ + {F E : obj-simplex-Category} (f : hom-simplex-Category F E) โ†’ coherence-square-maps - ( action-sSet P f) - ( map-hom-sSet Y) - ( map-hom-sSet X) - ( action-sSet Q f) + ( 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 P Q h + 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) โ†’ From b03cce90a97400e91566825d336a9d48259b15af Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 7 Jun 2025 11:48:50 +0100 Subject: [PATCH 7/7] edits set-magmoids --- ...ations-on-binary-families-of-sets.lagda.md | 15 +++++---- src/category-theory/set-magmoids.lagda.md | 33 +++++++++++-------- 2 files changed, 29 insertions(+), 19 deletions(-) diff --git a/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md b/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md index d4e50dfdf4..bf33a03810 100644 --- a/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md +++ b/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 _ diff --git a/src/category-theory/set-magmoids.lagda.md b/src/category-theory/set-magmoids.lagda.md index 27ed64102e..c037ebaff6 100644 --- a/src/category-theory/set-magmoids.lagda.md +++ b/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