{-# LANGUAGE GADTs, TypeOperators #-}
module Control.Category.Discrete
( Discrete(Refl)
, liftDiscrete
, cast
, inverse
) where
import Prelude ()
import Control.Category
data Discrete a b where
Refl :: Discrete a a
instance Category Discrete where
id :: Discrete a a
id = Discrete a a
forall a. Discrete a a
Refl
Refl . :: Discrete b c -> Discrete a b -> Discrete a c
. Refl = Discrete a c
forall a. Discrete a a
Refl
liftDiscrete :: Discrete a b -> Discrete (f a) (f b)
liftDiscrete :: Discrete a b -> Discrete (f a) (f b)
liftDiscrete Refl = Discrete (f a) (f b)
forall a. Discrete a a
Refl
cast :: Category k => Discrete a b -> k a b
cast :: Discrete a b -> k a b
cast Refl = k a b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
inverse :: Discrete a b -> Discrete b a
inverse :: Discrete a b -> Discrete b a
inverse Refl = Discrete b a
forall a. Discrete a a
Refl