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	|- TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctermc	|- TermCat
1		vc	|- c
2		cthinc	|- ThinCat
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- c
6	5 4	cfv	|- ( Base ` c )
7	3	cv	|- x
8	7	csn	|- { x }
9	6 8	wceq	|- ( Base ` c ) = { x }
10	9 3	wex	|- E. x ( Base ` c ) = { x }
11	10 1 2	crab	|- { c e. ThinCat | E. x ( Base ` c ) = { x } }
12	0 11	wceq	|- TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } }