Category theory

Examples of categories and large categories

Category	File
Groups	`group-theory.category-of-groups`
Semigroups	`group-theory.category-of-semigroups`

Examples of precategories and large precategories

Precategory	File
Abelian groups	`group-theory.precategory-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`
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`
Rings	`ring-theory.precategory-of-rings`
Semigroups	`group-theory.precategory-of-semigroups`
Semirings	`ring-theory.precategory-of-semirings`
Sets	`foundation.category-of-sets`

Files in the category theory folder

module category-theory where

open import category-theory.adjunctions-large-precategories public
open import category-theory.anafunctors public
open import category-theory.categories public
open import category-theory.coproducts-precategories public
open import category-theory.discrete-categories public
open import category-theory.endomorphisms-of-objects-categories public
open import category-theory.epimorphisms-large-precategories public
open import category-theory.equivalences-categories public
open import category-theory.equivalences-large-precategories public
open import category-theory.equivalences-precategories public
open import category-theory.exponential-objects-precategories public
open import category-theory.functors-categories public
open import category-theory.functors-large-precategories public
open import category-theory.functors-precategories public
open import category-theory.groupoids public
open import category-theory.homotopies-natural-transformations-large-precategories public
open import category-theory.initial-objects-precategories public
open import category-theory.isomorphisms-categories public
open import category-theory.isomorphisms-large-precategories public
open import category-theory.isomorphisms-precategories public
open import category-theory.large-categories public
open import category-theory.large-precategories public
open import category-theory.monomorphisms-large-precategories public
open import category-theory.natural-isomorphisms-categories public
open import category-theory.natural-isomorphisms-large-precategories public
open import category-theory.natural-isomorphisms-precategories public
open import category-theory.natural-numbers-object-precategories public
open import category-theory.natural-transformations-categories public
open import category-theory.natural-transformations-large-precategories public
open import category-theory.natural-transformations-precategories public
open import category-theory.opposite-precategories public
open import category-theory.precategories public
open import category-theory.precategory-of-functors public
open import category-theory.pregroupoids public
open import category-theory.products-of-precategories public
open import category-theory.products-precategories public
open import category-theory.pullbacks-precategories public
open import category-theory.sieves-categories public
open import category-theory.slice-precategories public
open import category-theory.terminal-objects-precategories public