-- | -- 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