{-# 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 :: forall a. Discrete a a
id = Discrete a a
forall a. Discrete a a
Refl
Discrete b c
Refl . :: forall b c a. Discrete b c -> Discrete a b -> Discrete a c
. Discrete a b
Refl = Discrete a c
forall a. Discrete a a
Refl
liftDiscrete :: Discrete a b -> Discrete (f a) (f b)
liftDiscrete :: forall a b (f :: * -> *). Discrete a b -> Discrete (f a) (f b)
liftDiscrete Discrete a b
Refl = Discrete (f a) (f b)
forall a. Discrete a a
Refl
cast :: Category k => Discrete a b -> k a b
cast :: forall (k :: * -> * -> *) a b. Category k => Discrete a b -> k a b
cast Discrete a b
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 :: forall a b. Discrete a b -> Discrete b a
inverse Discrete a b
Refl = Discrete b a
forall a. Discrete a a
Refl