Discrete category

A discrete category is a gaunt groupoid, #m/def/cat i.e. a category with only identity morphisms.

Sets as categories

Discrete categories correspond exactly to sets: For a given set $𝑋$ , we may form the set-as-category $𝑋 ――$ where

$𝑋 ―― 0 = 𝑋$ ;
$𝑋 ―― (𝑎, 𝑏) = (𝑎 \equiv 𝑋 𝑏)$ .

Moreover, if $𝑓 : 𝑋 \to 𝑌$ is a function then $𝑓 ―― : 𝑋 ―― \to 𝑌 ――$ is a functor defined so that for $𝑥 \in 𝑋$ , $𝑓 ―― 0 (𝑥) = 𝑓 (𝑥)$ and for $𝑓 ―― 1 (𝑝) = 𝑓 (𝑝)$ .

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