Definition df-termc 49505

Description: Definition of the proper class (termcnex 49608) 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 49518). 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 49547). TermCat is also the class of categories to which all categories have exactly one functor (dftermc2 49552). See also dftermc3 49563 where TermCat is defined as categories with exactly one disjointified arrow.

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

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

Having defined the terminal category, we can then use it to define the universal property of initial (dfinito4 49533) and terminal objects (dftermo4 49534). The universal properties provide an alternate proof of initoeu1 17913, termoeu1 17920, initoeu2 17918, and termoeu2 49270. Since terminal categories are terminal objects, all terminal categories are mutually isomorphic (termcciso 49548).

The dual concept is the initial category, or the empty category (Example 7.2(3) of [Adamek] p. 101). See 0catg 17589, 0thincg 49490, func0g 49121, 0funcg 49117, and initc 49123.

(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 49504	. 2 class TermCat
2		vc	. . . . . . 7 setvar 𝑐
3	2	cv 1540	. . . . . 6 class 𝑐
4		cbs 17115	. . . . . 6 class Base
5	3, 4	cfv 6476	. . . . 5 class (Base‘𝑐)
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1540	. . . . . 6 class 𝑥
8	7	csn 4571	. . . . 5 class {𝑥}
9	5, 8	wceq 1541	. . . 4 wff (Base‘𝑐) = {𝑥}
10	9, 6	wex 1780	. . 3 wff ∃𝑥(Base‘𝑐) = {𝑥}
11		cthinc 49449	. . 3 class ThinCat
12	10, 2, 11	crab 3395	. 2 class {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}
13	1, 12	wceq 1541	1 wff TermCat = {𝑐 ∈ ThinCat ∣ ∃𝑥(Base‘𝑐) = {𝑥}}

This definition is referenced by:  istermc  49506