Control.Category.Discrete

Documentation

data Discrete a b where

Category of discrete objects. The only arrows are identity arrows.

Constructors

Refl :: Discrete a a

Instances

Category * Discrete

liftDiscrete :: Discrete a b -> Discrete (f a) (f b)

Discrete a b acts as a proof that a = b, lift that proof into something of kind * -> *

cast :: Category k => Discrete a b -> k a b

Lower the proof that a ~ b to an arbitrary category.

inverse :: Discrete a b -> Discrete b a