    {-# LANGUAGE GADTs, TypeOperators #-}
    -------------------------------------------------------------------------------------------
    -- |
    -- Module    : Control.Category.Discrete
    -- Copyright : 2008-2010 Edward Kmett
    -- License   : BSD
    --
    -- Maintainer  : Edward Kmett <ekmett@gmail.com>
    -- Stability   : experimental
    -- Portability : portable
    --
    -------------------------------------------------------------------------------------------
    module Control.Category.Discrete
        ( Discrete(Refl)
        , liftDiscrete
        , cast
        , inverse
        ) where

    import Prelude ()
    import Control.Category

    -- | Category of discrete objects. The only arrows are identity arrows.
    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
    Discrete a a
    forall a. Discrete a a
    Refl

    -- instance Groupoid Discrete where
    --  inv Refl = Refl

    -- | Discrete a b acts as a proof that a = b, lift that proof into something of kind * -> *
    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 a)
    Discrete (f a) (f b)
    forall a. Discrete a a
    Refl

    -- | Lower the proof that a ~ b to an arbitrary category.
    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
    k b b
    forall a. k a a
    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
    Discrete b b
    forall a. Discrete a a
    Refl