diff --git a/Control/Arrow/Constrained.hs b/Control/Arrow/Constrained.hs
--- a/Control/Arrow/Constrained.hs
+++ b/Control/Arrow/Constrained.hs
@@ -80,6 +80,8 @@
 
 import qualified Control.Arrow as Arr
 
+import Control.Category.Discrete
+
 infixr 1 >>>, <<<
 infixr 3 &&&, ***
 
@@ -236,6 +238,13 @@
 instance (Category k) => EnhancedCat k k where
   arr = id
 
+instance EnhancedCat (->) Discrete where
+  arr Refl = id
+instance EnhancedCat Coercion Discrete where
+  arr Refl = id
+instance Category f => EnhancedCat (ConstrainedCategory f o) Discrete where
+  arr Refl = id
+
 -- | Many categories have as morphisms essentially /functions with extra properties/:
 --   group homomorphisms, linear maps, continuous functions...
 -- 
@@ -252,6 +261,8 @@
 f $ x = arr f x
 
 instance (Function f) => EnhancedCat (->) (ConstrainedCategory f o) where
+  arr (ConstrainedMorphism q) = arr q
+instance (EnhancedCat Discrete f) => EnhancedCat Discrete (ConstrainedCategory f o) where
   arr (ConstrainedMorphism q) = arr q
 
 instance EnhancedCat (->) Coercion where
diff --git a/Control/Category/Constrained.hs b/Control/Category/Constrained.hs
--- a/Control/Category/Constrained.hs
+++ b/Control/Category/Constrained.hs
@@ -53,6 +53,8 @@
 import Data.Type.Coercion
 import qualified Control.Category as Hask
 
+import Control.Category.Discrete
+
 -- | In mathematics, a category is defined as a class of /objects/, plus a class of
 --   /morphisms/ between those objects. In Haskell, one traditionally works in
 --   the category @(->)@ (called /Hask/), in which /any Haskell type/ is an object. 
@@ -75,6 +77,10 @@
 
 infixr 9 .
 
+instance Category Discrete where
+  id = Refl
+  Refl . Refl = Refl
+
 instance Category (->) where
   id = Prelude.id
   (.) = (Prelude..)
@@ -405,6 +411,9 @@
   alg f = f
   ($~) = ($)
 
+instance HasAgent Discrete where
+  alg = genericAlg
+  ($~) = genericAgentMap
 
 instance Category Coercion where
   id = Hask.id
diff --git a/Control/Category/Discrete.hs b/Control/Category/Discrete.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Discrete.hs
@@ -0,0 +1,25 @@
+-- |
+-- Module      :  Control.Category.Discrete
+-- Copyright   :  (c) 2018 Justus Sagemüller
+-- License     :  GPL v3 (see COPYING)
+-- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- 
+-- 
+{-# 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 = Refl
+   Refl . Refl = Refl
diff --git a/Control/Functor/Constrained.hs b/Control/Functor/Constrained.hs
--- a/Control/Functor/Constrained.hs
+++ b/Control/Functor/Constrained.hs
@@ -39,6 +39,9 @@
 import Data.Type.Coercion
 import Data.Complex
 
+import Control.Category.Discrete
+
+
 class ( Category r, Category t, Object t (f (UnitObject r)) )
            => Functor f r t | f r -> t, f t -> r where
   fmap :: (Object r a, Object t (f a), Object r b, Object t (f b))
@@ -109,4 +112,12 @@
 instance Functor ((,) a) Coercion Coercion where fmap Coercion = Coercion
 instance Functor IO Coercion Coercion where fmap Coercion = Coercion
 instance Functor Complex Coercion Coercion where fmap Coercion = Coercion
+
+instance Functor [] Discrete Discrete where fmap Refl = Refl
+instance Functor Maybe Discrete Discrete where fmap Refl = Refl
+instance Functor (Either a) Discrete Discrete where fmap Refl = Refl
+instance Functor ((->) a) Discrete Discrete where fmap Refl = Refl
+instance Functor ((,) a) Discrete Discrete where fmap Refl = Refl
+instance Functor IO Discrete Discrete where fmap Refl = Refl
+instance Functor Complex Discrete Discrete where fmap Refl = Refl
 
diff --git a/constrained-categories.cabal b/constrained-categories.cabal
--- a/constrained-categories.cabal
+++ b/constrained-categories.cabal
@@ -1,5 +1,5 @@
 Name:                constrained-categories
-Version:             0.3.0.1
+Version:             0.3.1.0
 Category:            control
 Synopsis:            Constrained clones of the category-theory type classes, using ConstraintKinds.
 Description:         Haskell has, and makes great use of, powerful facilities from category
@@ -54,6 +54,7 @@
                       Control.Arrow.Constrained
                       Control.Monad.Constrained
                       Control.Category.Hask
+                      Control.Category.Discrete
                       Control.Category.Constrained.Prelude
                       Control.Category.Constrained.Reified
                       Control.Category.Constrained.Reified.PolyPattern