Discrete n, the category with n objects, and as the only arrows their identities.
- data Z
- data S n = S n
- data Discrete where
- magicZ :: Discrete Z a b -> x
- magicZO :: Obj (Discrete Z) a -> x
- data Next where
- data DiscreteDiagram where
The arrows in Discrete n, a finite set of identity arrows.