Category theory
Content created by Fredrik Bakke, Egbert Rijke, 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 2025-02-10.
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 |
| Metric spaces and isometries | metric-spaces.category-of-metric-spaces-and-isometries |
| Metric spaces and short functions | metric-spaces.category-of-metric-spaces-and-short-functions |
| Rings | ring-theory.category-of-rings |
| Semigroups | group-theory.category-of-semigroups |
| Sets | foundation.category-of-sets |
Examples of precategories and large precategories
Modules in the category theory namespace
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.commuting-triangles-of-morphisms-in-precategories public open import category-theory.commuting-triangles-of-morphisms-in-set-magmoids public open import category-theory.complete-precategories public open import category-theory.composition-operations-on-binary-families-of-sets public open import category-theory.cones-precategories 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.coslice-precategories public open import category-theory.dependent-composition-operations-over-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.displayed-precategories 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.extensions-of-functors-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.limits-precategories 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.opposite-strongly-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.right-extensions-precategories public open import category-theory.right-kan-extensions-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.strongly-preunivalent-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
- 2025-02-10. Fredrik Bakke. Some extensions of the fundamental theorem of identity types (#1243).
- 2024-10-27. Fredrik Bakke. Displayed precategories (#922).
- 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
- 2024-08-29. Fernando Chu, Fredrik Bakke and Egbert Rijke. Cones, limits and reduced coslices of precats (#1161).
- 2024-08-05. Fernando Chu. Definition of ordinals (#1159).