# nLab finite category

Finite categories

category theory

# Finite categories

## Definition

A finite category $C$ is a category internal to the category FinSet of finite sets.

This means that a finite category consists of

(Notice that the latter implies the former, since for every object there is the identity morphism on that object). Finite categories form the 2-category, FinCat.

Similarly, a locally finite category is a category enriched over $Fin Set$, that is a category whose hom-sets are all finite.

(Locally) finite categories may also be called (locally) $\omega$-small; this generalises from $\omega$ (the set of natural numbers) to (other) inaccessible cardinals (or, equivalently, Grothendieck universes).

## Limits and colimits

One is often interested in whether an arbitrary category $D$ has limits and colimits indexed by finite categories. A category with all finite limits is called finitely complete or left exact (or lex for short). A category with all finite colimits is called finitely cocomplete or right exact.

## In dependent type theory

In dependent type theory, there are multiple notions of category. Because the type of objects in a category is required to be a finite set, all finite categories are strict categories, and the only finite univalent categories are the finite gaunt categories.

Last revised on July 25, 2023 at 17:54:01. See the history of this page for a list of all contributions to it.