Types of Category

Discrete category

A discrete category is a gaunt groupoid, #m/def/cat i.e. a category with only identity morphisms. Discrete categories correspond exactly to sets: For a given set 𝑋, we may form the set-as-category 𝑋―― where

• 𝑋――0 =𝑋;
• 𝑋――(𝑎,𝑏) =(𝑎 ≡𝑋𝑏).

#state/tidy | #lang/en | #SemBr