5.1. Internal categories [000O]

The notion of a (meta-)category is an essentially algebraic theory. As such it is possible to compute models of this theory in any category that has finite limits.

[001A] Definition 5.1·a (Internal category).

Let $E$ be a category with finite limits; then an internal category in $E$ is defined by the following data:

  1. an object of objects $C\Sub{0}\in E$,
  2. an object of morphisms $C\Sub{1}\in E$,
  3. source and target morphisms $s,t:C\Sub{1}\to C\Sub{0}$,
  4. a generic identity morphism $C\Sub{0}\to C\Sub{1}$,
  5. a generic composition morphism $C\Sub{1}\times\Sub{C\Sub{0}}C\Sub{1}\to C\Sub{1}$,
  6. satisfying a number of laws corresponding to those of a category.

For the details of these laws, we refer to the nLab (internal category).