Definition df-termc 49093

Description: Definition of the class 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 49104). These are exactly the thin categories with a singleton base set. Example 3.3(4.c) of [Adamek] p. 24. Followed directly from the definition, these categories are thin (termcthin 49097). As the name indicates, TermCat is the class of all terminal objects in the category of small categories (termcterm3 49120). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 49123). The opposite category of a terminal category is "almost" itself (oppctermco 49110).

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

The dual concept is the initial category, or the empty category. See 0catg 17727, 0thincg 49080, and 0funcg 48891.

(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 49092	. 2 class TermCat
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1539	. . . . . 6 class 𝑐
4		cbs 17243	. . . . . 6 class Base
5	3, 4	cfv 6559	. . . . 5 class (Base‘𝑐)
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1539	. . . . . 6 class 𝑥
8	7	csn 4624	. . . . 5 class {𝑥}
9	5, 8	wceq 1540	. . . 4 wff (Base‘𝑐) = {𝑥}
10	9, 6	wex 1779	. . 3 wff ∃𝑥(Base‘𝑐) = {𝑥}
11		cthinc 49040	. . 3 class ThinCat
12	10, 2, 11	crab 3435	. 2 class {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
13	1, 12	wceq 1540	1 wff TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}

This definition is referenced by:  istermc  49094