(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.

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.