Category theory

Content created by Egbert Rijke, Fredrik Bakke, Fernando Chu, Elisabeth Bonnevier, Jonathan Prieto-Cubides, Emily Riehl, Daniel Gratzer, Julian KG, fernabnor, Gregor Perčič and louismntnu.

Created on 2022-03-11.
Last modified on 2023-09-21.

Examples of categories and large categories

Examples of precategories and large precategories

Files in the category theory folder

module category-theory where

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.categories public
open import category-theory.coproducts-in-precategories public
open import category-theory.dependent-products-of-categories public
open import category-theory.dependent-products-of-precategories public
open import category-theory.discrete-categories 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.exponential-objects-in-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-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-large-categories public
open import category-theory.initial-objects-large-precategories public
open import category-theory.initial-objects-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.large-categories public
open import category-theory.large-precategories public
open import category-theory.monomorphisms-in-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.one-object-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-in-precategories public
open import category-theory.products-of-precategories public
open import category-theory.pullbacks-in-precategories public
open import category-theory.representable-functors-categories public
open import category-theory.representable-functors-precategories public
open import category-theory.sieves-in-categories public
open import category-theory.slice-precategories public
open import category-theory.terminal-objects-in-precategories public
open import category-theory.yoneda-lemma-categories public
open import category-theory.yoneda-lemma-precategories public

Recent changes