Definition df-termc

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 ). 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 ). As the name indicates, TermCat is the class of all terminal objects in the category of small categories ( termcterm3 ). TermCat is also the class of categories to which all categories have exactly one functor ( dftermc2 ). The opposite category of a terminal category is "almost" itself ( oppctermco ).

Unlike https://ncatlab.org/nlab/show/terminal+category , we reserve the term "trivial category" for ( SetCat1o ) , justified by setc1oterm .

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

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

	Ref	Expression
Assertion	df-termc	Could not format assertion : No typesetting found for |- TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctermc	Could not format TermCat : No typesetting found for class TermCat with typecode class
1		vc	$$setvarc$$
2		cthinc	$$class\mathrm{ThinCat}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class{\mathrm{Base}}_c$$
7	3	cv	$$setvarx$$
8	7	csn	$$class\left\{x\right\}$$
9	6 8	wceq	$$wff{\mathrm{Base}}_c=\left\{x\right\}$$
10	9 3	wex	$$wff\exists x{\mathrm{Base}}_c=\left\{x\right\}$$
11	10 1 2	crab	$$class\left\{c\in \mathrm{ThinCat}|\exists x{\mathrm{Base}}_c=\left\{x\right\}\right\}$$
12	0 11	wceq	Could not format TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } } : No typesetting found for wff TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } } with typecode wff