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 = { 𝑐 ∈ ThinCat ∣ ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctermc	⊢ TermCat
1		vc	⊢ 𝑐
2		cthinc	⊢ ThinCat
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Base ‘ 𝑐 )
7	3	cv	⊢ 𝑥
8	7	csn	⊢ { 𝑥 }
9	6 8	wceq	⊢ ( Base ‘ 𝑐 ) = { 𝑥 }
10	9 3	wex	⊢ ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 }
11	10 1 2	crab	⊢ { 𝑐 ∈ ThinCat ∣ ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } }
12	0 11	wceq	⊢ TermCat = { 𝑐 ∈ ThinCat ∣ ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } }