Category theory
Content created by Egbert Rijke, Fredrik Bakke, Fernando Chu, Elisabeth Stenholm, Daniel Gratzer, Jonathan Prieto-Cubides, Emily Riehl, Gregor Perčič, Julian KG, Vojtěch Štěpančík, fernabnor and louismntnu.
Created on 2022-03-11.
Last modified on 2024-02-08.
Examples of categories and large categories
| Category | File |
|---|---|
| Abelian groups | group-theory.category-of-abelian-groups |
| Commutative Rings | commutative-algebra.category-of-commutative-rings |
| Connected set bundles over 𝕊¹ | synthetic-homotopy-theory.category-of-connected-set-bundles-circle |
| Families of sets | foundation.category-of-families-of-sets |
| Groups | group-theory.category-of-groups |
G-sets | group-theory.category-of-group-actions |
| Rings | ring-theory.category-of-rings |
| Semigroups | group-theory.category-of-semigroups |
| Sets | foundation.category-of-sets |
Examples of precategories and large precategories
| Precategory | File |
|---|---|
| Abelian groups | group-theory.category-of-abelian-groups |
| Commutative monoids | group-theory.precategory-of-commutative-monoids |
| Commutative rings | commutative-algebra.precategory-of-commutative-rings |
| Commutative semirings | commutative-algebra.precategory-of-commutative-semirings |
| Concrete groups | group-theory.precategory-of-concrete-groups |
| Decidable total orders | order-theory.precategory-of-decidable-total-orders |
| Finite species | species.precategory-of-finite-species |
G-sets | group-theory.precategory-of-group-actions |
| Groups | group-theory.precategory-of-groups |
| Monoids | group-theory.precategory-of-monoids |
| Posets | order-theory.precategory-of-posets |
| Rings | ring-theory.precategory-of-rings |
| Semigroups | group-theory.precategory-of-semigroups |
| Semirings | ring-theory.precategory-of-semirings |
| Sets | foundation.category-of-sets |
| Total orders | order-theory.precategory-of-total-orders |
Files in the category theory folder
module category-theory where open import category-theory.adjunctions-large-categories public open import category-theory.adjunctions-large-precategories public open import category-theory.anafunctors-categories public open import category-theory.anafunctors-precategories public open import category-theory.augmented-simplex-category public open import category-theory.categories public 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.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 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 open import category-theory.cores-precategories public open import category-theory.dependent-products-of-categories public open import category-theory.dependent-products-of-large-categories public open import category-theory.dependent-products-of-large-precategories public open import category-theory.dependent-products-of-precategories public open import category-theory.discrete-categories public open import category-theory.embedding-maps-precategories public open import category-theory.embeddings-precategories public open import category-theory.endomorphisms-in-categories public open import category-theory.endomorphisms-in-precategories public open import category-theory.epimorphisms-in-large-precategories public open import category-theory.equivalences-of-categories public open import category-theory.equivalences-of-large-precategories public open import category-theory.equivalences-of-precategories public open import category-theory.essential-fibers-of-functors-precategories public open import category-theory.essentially-injective-functors-precategories public open import category-theory.essentially-surjective-functors-precategories public open import category-theory.exponential-objects-precategories public open import category-theory.faithful-functors-precategories public open import category-theory.faithful-maps-precategories public open import category-theory.full-functors-precategories public open import category-theory.full-large-subcategories public open import category-theory.full-large-subprecategories public open import category-theory.full-maps-precategories public open import category-theory.full-subcategories public open import category-theory.full-subprecategories public open import category-theory.fully-faithful-functors-precategories public open import category-theory.fully-faithful-maps-precategories public open import category-theory.function-categories public open import category-theory.function-precategories public open import category-theory.functors-categories public open import category-theory.functors-from-small-to-large-categories public open import category-theory.functors-from-small-to-large-precategories public open import category-theory.functors-large-categories public open import category-theory.functors-large-precategories public open import category-theory.functors-nonunital-precategories public open import category-theory.functors-precategories public open import category-theory.functors-set-magmoids public open import category-theory.gaunt-categories public open import category-theory.groupoids public open import category-theory.homotopies-natural-transformations-large-precategories public open import category-theory.indiscrete-precategories public open import category-theory.initial-category public open import category-theory.initial-objects-large-categories public open import category-theory.initial-objects-large-precategories public open import category-theory.initial-objects-precategories public open import category-theory.isomorphism-induction-categories public open import category-theory.isomorphism-induction-precategories public open import category-theory.isomorphisms-in-categories public open import category-theory.isomorphisms-in-large-categories public open import category-theory.isomorphisms-in-large-precategories public open import category-theory.isomorphisms-in-precategories public open import category-theory.isomorphisms-in-subprecategories public open import category-theory.large-categories public open import category-theory.large-function-categories public open import category-theory.large-function-precategories public open import category-theory.large-precategories public open import category-theory.large-subcategories public open import category-theory.large-subprecategories public open import category-theory.maps-categories public open import category-theory.maps-from-small-to-large-categories public open import category-theory.maps-from-small-to-large-precategories public open import category-theory.maps-precategories public open import category-theory.maps-set-magmoids public open import category-theory.monads-on-categories public open import category-theory.monads-on-precategories public open import category-theory.monomorphisms-in-large-precategories public open import category-theory.natural-isomorphisms-functors-categories public open import category-theory.natural-isomorphisms-functors-large-precategories public open import category-theory.natural-isomorphisms-functors-precategories public open import category-theory.natural-isomorphisms-maps-categories public open import category-theory.natural-isomorphisms-maps-precategories public open import category-theory.natural-numbers-object-precategories public open import category-theory.natural-transformations-functors-categories public open import category-theory.natural-transformations-functors-from-small-to-large-categories public open import category-theory.natural-transformations-functors-from-small-to-large-precategories public open import category-theory.natural-transformations-functors-large-categories public open import category-theory.natural-transformations-functors-large-precategories public open import category-theory.natural-transformations-functors-precategories public open import category-theory.natural-transformations-maps-categories public open import category-theory.natural-transformations-maps-from-small-to-large-precategories public open import category-theory.natural-transformations-maps-precategories public open import category-theory.nonunital-precategories public open import category-theory.one-object-precategories public open import category-theory.opposite-categories public open import category-theory.opposite-large-precategories public open import category-theory.opposite-precategories public open import category-theory.opposite-preunivalent-categories public open import category-theory.pointed-endofunctors-categories public open import category-theory.pointed-endofunctors-precategories public open import category-theory.precategories public open import category-theory.precategory-of-elements-of-a-presheaf public open import category-theory.precategory-of-functors public open import category-theory.precategory-of-functors-from-small-to-large-precategories public open import category-theory.precategory-of-maps-from-small-to-large-precategories public open import category-theory.precategory-of-maps-precategories public open import category-theory.pregroupoids public open import category-theory.presheaf-categories public open import category-theory.preunivalent-categories public open import category-theory.products-in-precategories public open import category-theory.products-of-precategories public open import category-theory.pseudomonic-functors-precategories public open import category-theory.pullbacks-in-precategories public open import category-theory.replete-subprecategories public open import category-theory.representable-functors-categories public open import category-theory.representable-functors-large-precategories public open import category-theory.representable-functors-precategories public open import category-theory.representing-arrow-category public open import category-theory.restrictions-functors-cores-precategories public open import category-theory.rigid-objects-categories public open import category-theory.rigid-objects-precategories public open import category-theory.set-magmoids public open import category-theory.sieves-in-categories public open import category-theory.simplex-category public open import category-theory.slice-precategories public open import category-theory.split-essentially-surjective-functors-precategories public 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 open import category-theory.wide-subprecategories public open import category-theory.yoneda-lemma-categories public open import category-theory.yoneda-lemma-precategories public
Recent changes
- 2024-02-08. Egbert Rijke. Refactor the definition of monads (#1019).
- 2024-02-06. Gregor Perčič. Definition of monads on precategories and categories (+ of whiskering and horizontal composition) (#1018).
- 2023-11-27. Elisabeth Stenholm, Daniel Gratzer and Egbert Rijke. Additions during work on material set theory in HoTT (#910).
- 2023-11-27. Fredrik Bakke. Refactor categories to carry a bidirectional witness of associativity (#945).
- 2023-11-24. Fredrik Bakke. Subterminal precategories and constant functors (#941).