Definition df-termc 50284

Description: Definition of the proper class (termcnex 50387) 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 50297). 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 50326). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 50331). See also dftermc3 50342 where TermCat is defined as categories with exactly one disjointified arrow.

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

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

Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 50312) and terminal objects (dftermo4 50313). The universal properties provide an alternate proof of initoeu1 18086, termoeu1 18093, initoeu2 18091, and termoeu2 50049. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 50327).

The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17762, 0thincg 50269, func0g 49900, 0funcg 49896, and initc 49902.

(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 50283	. 2 class TermCat
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1569	. . . . . 6 class 𝑐
4		cbs 17287	. . . . . 6 class Base
5	3, 4	cfv 6540	. . . . 5 class (Base‘𝑐)
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1569	. . . . . 6 class 𝑥
8	7	csn 4591	. . . . 5 class {𝑥}
9	5, 8	wceq 1570	. . . 4 wff (Base‘𝑐) = {𝑥}
10	9, 6	wex 1812	. . 3 wff ∃𝑥(Base‘𝑐) = {𝑥}
11		cthinc 50228	. . 3 class ThinCat
12	10, 2, 11	crab 3418	. 2 class {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
13	1, 12	wceq 1570	1 wff TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}

This definition is used by:  istermc  50285