-- |
-- Module      :  Control.Category.Discrete
-- Copyright   :  (c) 2018 Justus Sagemüller
-- License     :  GPL v3 (see COPYING)
-- Maintainer  :  (@) jsag $ hvl.no
-- 
-- 
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE PolyKinds            #-}


module Control.Category.Discrete where

import Control.Category

-- | The discrete category is the category with the minimum possible amount
--   of arrows: for any given type, there is 'id', and that's all.
--   You can use this to provide a proof that some endomorphism (of not closer
--   specified category) is the identity.
data Discrete a b where
   Refl :: Discrete a a

instance Category Discrete where
   id :: Discrete a a
id = Discrete a a
forall k (a :: k). Discrete a a
Refl
   Discrete b c
Refl . :: Discrete b c -> Discrete a b -> Discrete a c
. Discrete a b
Refl = Discrete a c
forall k (a :: k). Discrete a a
Refl