Definition df-termc 49960

Description: Definition of the proper class (termcnex 50063) 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 49973). 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 50002). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 50007). See also dftermc3 50018 where TermCat is defined as categories with exactly one disjointified arrow.

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

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

Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 49988) and terminal objects (dftermo4 49989). The universal properties provide an alternate proof of initoeu1 17969, termoeu1 17976, initoeu2 17974, and termoeu2 49725. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 50003).

The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17645, 0thincg 49945, func0g 49576, 0funcg 49572, and initc 49578.

(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 49959	. 2 class TermCat
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1541	. . . . . 6 class 𝑐
4		cbs 17170	. . . . . 6 class Base
5	3, 4	cfv 6492	. . . . 5 class (Base‘𝑐)
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1541	. . . . . 6 class 𝑥
8	7	csn 4568	. . . . 5 class {𝑥}
9	5, 8	wceq 1542	. . . 4 wff (Base‘𝑐) = {𝑥}
10	9, 6	wex 1781	. . 3 wff ∃𝑥(Base‘𝑐) = {𝑥}
11		cthinc 49904	. . 3 class ThinCat
12	10, 2, 11	crab 3390	. 2 class {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
13	1, 12	wceq 1542	1 wff TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}

This definition is referenced by:  istermc  49961