Definition df-termc 49172

Description: Definition of the proper class (termcnex 49268) of terminal categories, or final categories, i.e., categories with exactly one object and exactly one morphism, the latter of which is an identity morphism (termcid 49184). These are exactly the thin categories with a singleton base set. Example 3.3(4.c) of [Adamek] p. 24.

As the name indicates, TermCat is the class of all terminal objects in the category of small categories (termcterm3 49213). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 49218). See also dftermc3 49229 where TermCat is defined as categories with exactly one disjointified arrow.

Unlike https://ncatlab.org/nlab/show/terminal+category 49229, we reserve the term "trivial category" for (SetCat‘1_o), justified by setc1oterm 49189.

Followed directly from the definition, terminal categories are thin (termcthin 49176). The opposite category of a terminal category is "almost" itself (oppctermco 49203). Any category 𝐶 is isomorphic to the category of functors from a terminal category to the category 𝐶 (diagcic 49238).

Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 49199) and terminal objects (dftermo4 49200). The universal properties provide an alternate proof of initoeu1 18028, termoeu1 18035, initoeu2 18033, and termoeu2 48989. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 49214).

The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17703, 0thincg 49159, and 0funcg 48943.

(Contributed by Zhi Wang, 16-Oct-2025.)

Assertion

Ref	Expression
df-termc	⊢ TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}

Distinct variable group:   𝑥,𝑐

Detailed syntax breakdown of Definition df-termc

Step	Hyp	Ref	Expression
1		ctermc 49171	. 2 class TermCat
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1538	. . . . . 6 class 𝑐
4		cbs 17230	. . . . . 6 class Base
5	3, 4	cfv 6541	. . . . 5 class (Base‘𝑐)
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1538	. . . . . 6 class 𝑥
8	7	csn 4606	. . . . 5 class {𝑥}
9	5, 8	wceq 1539	. . . 4 wff (Base‘𝑐) = {𝑥}
10	9, 6	wex 1778	. . 3 wff ∃𝑥(Base‘𝑐) = {𝑥}
11		cthinc 49118	. . 3 class ThinCat
12	10, 2, 11	crab 3419	. 2 class {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
13	1, 12	wceq 1539	1 wff TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}

This definition is referenced by:  istermc  49173