diff --git a/Control/Applicative/Constrained.hs b/Control/Applicative/Constrained.hs
--- a/Control/Applicative/Constrained.hs
+++ b/Control/Applicative/Constrained.hs
@@ -91,8 +91,8 @@
 
 constrainedFZipWith :: ( Category r, Category t, o a, o b, o (a,b), o c
                                                , o (f a, f b), o (f c) )
-        =>  ( r (a, b) c -> t (f a, f b) (f c) )
-         -> ConstrainedCategory r o (a, b) c -> ConstrainedCategory t o (f a, f b) (f c)
+        =>  (   r  (a, b) c ->    t  (f a, f b) (f c) )
+          -> (o⊢r) (a, b) c -> (o⊢t) (f a, f b) (f c)
 constrainedFZipWith zf = constrained . zf . unconstrained
          
 
diff --git a/Control/Arrow/Constrained.hs b/Control/Arrow/Constrained.hs
--- a/Control/Arrow/Constrained.hs
+++ b/Control/Arrow/Constrained.hs
@@ -82,6 +82,8 @@
 
 import Control.Category.Discrete
 
+import qualified Data.Functor.Contravariant as Hask
+
 infixr 1 >>>, <<<
 infixr 3 &&&, ***
 
@@ -242,7 +244,7 @@
   arr Refl = id
 instance EnhancedCat Coercion Discrete where
   arr Refl = id
-instance Category f => EnhancedCat (ConstrainedCategory f o) Discrete where
+instance Category f => EnhancedCat (o⊢f) Discrete where
   arr Refl = id
 
 -- | Many categories have as morphisms essentially /functions with extra properties/:
@@ -260,9 +262,9 @@
 ($) :: (Function f, Object f a, Object f b) => f a b -> a -> b
 f $ x = arr f x
 
-instance (Function f) => EnhancedCat (->) (ConstrainedCategory f o) where
+instance (Function f) => EnhancedCat (->) (o⊢f) where
   arr (ConstrainedMorphism q) = arr q
-instance (EnhancedCat Discrete f) => EnhancedCat Discrete (ConstrainedCategory f o) where
+instance (EnhancedCat Discrete f) => EnhancedCat Discrete (o⊢f) where
   arr (ConstrainedMorphism q) = arr q
 
 instance EnhancedCat (->) Coercion where
@@ -305,71 +307,78 @@
   unit = Hask.pure ()
   const = Hask.const
 
-constrainedArr :: (Category k, Category a, o b, o c )
-  => ( k b c                        -> a b c  )
-     -> k b c -> ConstrainedCategory a o b c
+constrainedArr :: (Category k, Category a, o b, o c ) => ( k b c ->    a  b c )
+                                                        -> k b c -> (o⊢a) b c
 constrainedArr ar = constrained . ar
 
 constrainedFirst :: ( Category a, Cartesian a, ObjectPair a b d, ObjectPair a c d )
-  => ( a b c -> a (b, d) (c, d) )
-     -> ConstrainedCategory a o b c -> ConstrainedCategory a o (b, d) (c, d)
+  => (    a  b c ->    a  (b, d) (c, d) )
+    -> (o⊢a) b c -> (o⊢a) (b, d) (c, d)
 constrainedFirst fs = ConstrainedMorphism . fs . unconstrained
   
 constrainedSecond :: ( Category a, Cartesian a, ObjectPair a d b, ObjectPair a d c )
-  => ( a b c -> a (d, b) (d, c) )
-     -> ConstrainedCategory a o b c -> ConstrainedCategory a o (d, b) (d, c)
+  => (    a  b c ->    a  (d, b) (d, c) )
+    -> (o⊢a) b c -> (o⊢a) (d, b) (d, c)
 constrainedSecond sn = ConstrainedMorphism . sn . unconstrained
 
+instance Morphism Hask.Op where
+  first (Hask.Op f) = Hask.Op $ first f
+  second (Hask.Op f) = Hask.Op $ second f
+  Hask.Op f *** Hask.Op g = Hask.Op $ f *** g
+instance MorphChoice Hask.Op where
+  left (Hask.Op f) = Hask.Op $ left f
+  right (Hask.Op f) = Hask.Op $ right f
+  Hask.Op f +++ Hask.Op g = Hask.Op $ f +++ g
 
-instance (Morphism a, o (UnitObject a)) => Morphism (ConstrainedCategory a o) where
+instance (Morphism a, o (UnitObject a)) => Morphism (o⊢a) where
   first = constrainedFirst first
   second = constrainedSecond second
   ConstrainedMorphism a *** ConstrainedMorphism b = ConstrainedMorphism $ a *** b
   
-instance (PreArrow a, o (UnitObject a)) => PreArrow (ConstrainedCategory a o) where
+instance (PreArrow a, o (UnitObject a)) => PreArrow (o⊢a) where
   ConstrainedMorphism a &&& ConstrainedMorphism b = ConstrainedMorphism $ a &&& b
   terminal = ConstrainedMorphism terminal
   fst = ConstrainedMorphism fst
   snd = ConstrainedMorphism snd
 
-instance (WellPointed a, o (UnitObject a)) => WellPointed (ConstrainedCategory a o) where
-  type PointObject (ConstrainedCategory a o) x = PointObject a x
+instance (WellPointed a, o (UnitObject a)) => WellPointed (o⊢a) where
+  type PointObject (o⊢a) x = PointObject a x
   globalElement x = ConstrainedMorphism $ globalElement x
   unit = cstrCatUnit
   const x = ConstrainedMorphism $ const x
 
 cstrCatUnit :: forall a o . (WellPointed a, o (UnitObject a))
-        => CatTagged (ConstrainedCategory a o) (UnitObject a)
+        => CatTagged (o⊢a) (UnitObject a)
 cstrCatUnit = retag (unit :: CatTagged a (UnitObject a))
   
 instance (EnhancedCat a k, o (UnitObject a))
-            => EnhancedCat (ConstrainedCategory a o) k where
+            => EnhancedCat (o⊢a) k where
   arr = constrainedArr arr
 
 
 constrainedLeft :: ( CoCartesian k, ObjectSum k b d, ObjectSum k c d )
-  => ( k b c -> k (b+d) (c+d) )
-     -> ConstrainedCategory k o b c -> ConstrainedCategory k o (b+d) (c+d)
+  => (    k  b c ->    k  (b+d) (c+d) )
+    -> (o⊢k) b c -> (o⊢k) (b+d) (c+d)
 constrainedLeft fs = ConstrainedMorphism . fs . unconstrained
   
 constrainedRight :: ( CoCartesian k, ObjectSum k b c, ObjectSum k b d )
-  => ( k c d -> k (b+c) (b+d) )
-     -> ConstrainedCategory k o c d -> ConstrainedCategory k o (b+c) (b+d)
+  => (    k  c d ->    k  (b+c) (b+d) )
+    -> (o⊢k) c d -> (o⊢k) (b+c) (b+d)
 constrainedRight fs = ConstrainedMorphism . fs . unconstrained
 
-instance (MorphChoice k, o (ZeroObject k)) => MorphChoice (ConstrainedCategory k o) where
+instance (MorphChoice k, o (ZeroObject k)) => MorphChoice (o⊢k) where
   left = constrainedLeft left
   right = constrainedRight right
   ConstrainedMorphism a +++ ConstrainedMorphism b = ConstrainedMorphism $ a +++ b
   
-instance (PreArrChoice k, o (ZeroObject k)) => PreArrChoice (ConstrainedCategory k o) where
+instance (PreArrChoice k, o (ZeroObject k)) => PreArrChoice (o⊢k) where
   ConstrainedMorphism a ||| ConstrainedMorphism b = ConstrainedMorphism $ a ||| b
   initial = ConstrainedMorphism initial
   coFst = ConstrainedMorphism coFst
   coSnd = ConstrainedMorphism coSnd
 
 instance (SPDistribute k, o (ZeroObject k), o (UnitObject k))
-     => SPDistribute (ConstrainedCategory k o) where
+     => SPDistribute (o⊢k) where
   distribute = ConstrainedMorphism distribute
   unDistribute = ConstrainedMorphism unDistribute
   boolAsSwitch = ConstrainedMorphism boolAsSwitch
diff --git a/Control/Category/Constrained.hs b/Control/Category/Constrained.hs
--- a/Control/Category/Constrained.hs
+++ b/Control/Category/Constrained.hs
@@ -13,6 +13,7 @@
 {-# LANGUAGE MultiParamTypeClasses        #-}
 {-# LANGUAGE FlexibleContexts             #-}
 {-# LANGUAGE RankNTypes                   #-}
+{-# LANGUAGE UnicodeSyntax                #-}
 {-# LANGUAGE AllowAmbiguousTypes          #-}
 {-# LANGUAGE TypeOperators                #-}
 {-# LANGUAGE ExplicitNamespaces           #-}
@@ -20,6 +21,7 @@
 #if __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE UndecidableSuperClasses      #-}
 #endif
+{-# LANGUAGE LambdaCase                   #-}
 
 module Control.Category.Constrained ( 
             -- * The category class
@@ -30,10 +32,13 @@
             -- * Monoidal with coproducts
           , type (+)()
           , CoCartesian (..), ObjectSum
+            -- * The standard function category
+          , type Hask
             -- * Isomorphisms
           , Isomorphic (..)
             -- * Constraining a category
           , ConstrainedCategory (ConstrainedMorphism)
+          , type (⊢)()
           , constrained, unconstrained
           , ConstrainedFunction
             -- * Global-element proxies
@@ -53,7 +58,10 @@
 import Data.Void
 import Data.Type.Coercion
 import qualified Control.Category as Hask
+import qualified Data.Functor.Contravariant as Hask (Op(..))
 
+import Data.Constraint.Trivial (Unconstrained)
+
 import Control.Category.Discrete
 
 -- | In mathematics, a category is defined as a class of /objects/, plus a class of
@@ -86,6 +94,21 @@
   id = Prelude.id
   (.) = (Prelude..)
 
+instance Category Hask.Op where
+  id = Hask.id
+  (.) = (Hask..)
+
+-- | The category of all Haskell types, with (wrapped) Haskell functions as morphisms.
+--   This is just a type-wrapper, morally equivalent to the @(->)@ category itself.
+--   The difference is that 'Control.Functor.Constrained.Functor' instances in the '(->)'
+--   category are automatically inherited from the standard 'Prelude.Functor' instances
+--   that most packages define their type for. The benefit of that is that normal
+--   Haskell code keeps working when the "Prelude" classes are replaced with the ones
+--   from this library, but the downside is that you can't make /more gradual/ instances
+--   when this is desired. This is where the 'Hask' category comes in: it only has functors
+--   that are explicitly declared as such.
+type Hask = Unconstrained⊢(->)
+
 -- | Analogue to 'asTypeOf', this does not actually do anything but can
 --   give the compiler type unification hints in a convenient manner.
 inCategoryOf :: (Category k) => k a b -> k c d -> k a b
@@ -95,15 +118,22 @@
 -- | A given category can be specialised, by using the same morphisms but adding
 --   extra constraints to what is considered an object. 
 -- 
---   For instance, @'ConstrainedCategory' (->) 'Ord'@ is the category of all
+--   For instance, @'Ord'⊢(->)@ is the category of all
 --   totally ordered data types (but with arbitrary functions; this does not require
 --   monotonicity or anything).
 newtype ConstrainedCategory (k :: * -> * -> *) (o :: * -> Constraint) (a :: *) (b :: *)
    = ConstrainedMorphism { unconstrainedMorphism :: k a b }
 
+type o ⊢ k = ConstrainedCategory k o
+
 -- | Cast a morphism to its equivalent in a more constrained category,
 --   provided it connects objects that actually satisfy the extra constraint.
-constrained :: (Category k, o a, o b) => k a b -> ConstrainedCategory k o a b
+-- 
+--   In practice, it is often necessary to specify to what typeclass it should be
+--   constrained. The most convenient way of doing that is with
+--   <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeApplications type-applications syntax>.
+--   E.g. @'constrained' \@Ord length@ is the 'length' function considered as a morphism in the subcategory of Hask in which all types are orderable. (Which makes it suitable for e.g. fmapping over a set.)
+constrained :: ∀ o k a b . (Category k, o a, o b) => k a b -> (o⊢k) a b
 constrained = ConstrainedMorphism
 
 -- | \"Unpack\" a constrained morphism again (forgetful functor).
@@ -112,11 +142,11 @@
 --   morphisms that are actually 'Function's can just be applied
 --   to their objects with '$' right away, no need to go back to
 --   Hask first.
-unconstrained :: (Category k) => ConstrainedCategory k o a b -> k a b
+unconstrained :: ∀ o k a b . (Category k) => (o⊢k) a b -> k a b
 unconstrained = unconstrainedMorphism
 
-instance (Category k) => Category (ConstrainedCategory k isObj) where
-  type Object (ConstrainedCategory k isObj) o = (Object k o, isObj o)
+instance (Category k) => Category (isObj⊢k) where
+  type Object (isObj⊢k) o = (Object k o, isObj o)
   id = ConstrainedMorphism id
   ConstrainedMorphism f . ConstrainedMorphism g = ConstrainedMorphism $ f . g
 
@@ -214,8 +244,8 @@
   
   swap :: ( ObjectPair k a b, ObjectPair k b a ) => k (a,b) (b,a)
   
-  attachUnit :: ( u ~ UnitObject k, ObjectPair k a u ) => k a (a,u)
-  detachUnit :: ( u ~ UnitObject k, ObjectPair k a u ) => k (a,u) a
+  attachUnit :: ( unit ~ UnitObject k, ObjectPair k a unit ) => k a (a,unit)
+  detachUnit :: ( unit ~ UnitObject k, ObjectPair k a unit ) => k (a,unit) a
   regroup    :: ( ObjectPair k a b, ObjectPair k b c
                 , ObjectPair k a (b,c), ObjectPair k (a,b) c
                 ) => k (a, (b, c)) ((a, b), c)
@@ -234,10 +264,17 @@
   detachUnit = \(a, ()) -> a
   regroup = \(a, (b, c)) -> ((a, b), c)
   regroup' = \((a, b), c) -> (a, (b, c))
+
+instance Cartesian Hask.Op where
+  swap = Hask.Op $ \(a,b) -> (b,a)
+  attachUnit = Hask.Op $ \(a, ()) -> a
+  detachUnit = Hask.Op $ \a -> (a, ())
+  regroup = Hask.Op $ \((a, b), c) -> (a, (b, c))
+  regroup' = Hask.Op $ \(a, (b, c)) -> ((a, b), c)
                         
-instance (Cartesian f, o (UnitObject f)) => Cartesian (ConstrainedCategory f o) where
-  type PairObjects (ConstrainedCategory f o) a b = (PairObjects f a b)
-  type UnitObject (ConstrainedCategory f o) = UnitObject f
+instance (Cartesian f, o (UnitObject f)) => Cartesian (o⊢f) where
+  type PairObjects (o⊢f) a b = (PairObjects f a b)
+  type UnitObject (o⊢f) = UnitObject f
 
   swap = ConstrainedMorphism swap
   attachUnit = ConstrainedMorphism attachUnit
@@ -272,8 +309,8 @@
   
   coSwap :: ( ObjectSum k a b, ObjectSum k b a ) => k (a+b) (b+a)
   
-  attachZero :: ( Object k a, z ~ ZeroObject k, ObjectSum k a z ) => k a (a+z)
-  detachZero :: ( Object k a, z ~ ZeroObject k, ObjectSum k a z ) => k (a+z) a
+  attachZero :: ( Object k a, zero ~ ZeroObject k, ObjectSum k a zero ) => k a (a+zero)
+  detachZero :: ( Object k a, zero ~ ZeroObject k, ObjectSum k a zero ) => k (a+zero) a
   coRegroup  :: ( Object k a, Object k c, ObjectSum k a b, ObjectSum k b c
                 , ObjectSum k a (b+c), ObjectSum k (a+b) c
                 ) => k (a+(b+c)) ((a+b)+c)
@@ -319,10 +356,31 @@
 --   boolFromSwitch (Left x) = (False,x)
 --   boolFromSwitch (Right x) = (True,x)
 --                         
-instance (CoCartesian f, o (ZeroObject f)) => CoCartesian (ConstrainedCategory f o) where
-  type SumObjects (ConstrainedCategory f o) a b = (SumObjects f a b)
-  type ZeroObject (ConstrainedCategory f o) = ZeroObject f
+instance CoCartesian Hask.Op where
+  coSwap = Hask.Op $ \case Right a -> Left a
+                           Left a -> Right a
+  attachZero = Hask.Op $ \case Left a -> a
+                               Right void -> absurd void
+  detachZero = Hask.Op Left
+  coRegroup = Hask.Op $ \case Left (Left a) -> Left a
+                              Left (Right a) -> (Right (Left a))
+                              Right a -> Right (Right a)
+  coRegroup' = Hask.Op $ \case (Left a) -> Left (Left a)
+                               Right (Left a) -> Left (Right a)
+                               Right (Right a) -> Right a
+  maybeFromSum = Hask.Op $ \case Nothing -> Left ()
+                                 Just x -> Right x
+  maybeAsSum = Hask.Op $ \case Left () -> Nothing
+                               Right x -> Just x
+  boolFromSum = Hask.Op $ \case False -> Left ()
+                                True -> Right ()
+  boolAsSum = Hask.Op $ \case Left () -> False
+                              Right () -> True
 
+instance (CoCartesian f, o (ZeroObject f)) => CoCartesian (o⊢f) where
+  type SumObjects (o⊢f) a b = (SumObjects f a b)
+  type ZeroObject (o⊢f) = ZeroObject f
+
   coSwap = ConstrainedMorphism coSwap
   attachZero = ConstrainedMorphism attachZero
   detachZero = ConstrainedMorphism detachZero
@@ -369,8 +427,8 @@
   apply (f,x) = f x
       
 
-instance (Curry f, o (UnitObject f)) => Curry (ConstrainedCategory f o) where
-  type MorphObjects (ConstrainedCategory f o) a c = ( MorphObjects f a c, f ~ (->) )
+instance (Curry f, o (UnitObject f)) => Curry (o⊢f) where
+  type MorphObjects (o⊢f) a c = ( MorphObjects f a c, f ~ (->) )
   uncurry (ConstrainedMorphism f) = ConstrainedMorphism $ \(a,b) -> unconstrained (f a) b
   curry (ConstrainedMorphism f) = ConstrainedMorphism $ \a -> ConstrainedMorphism $ \b -> f (a, b)
                                                                      
diff --git a/Control/Functor/Constrained.hs b/Control/Functor/Constrained.hs
--- a/Control/Functor/Constrained.hs
+++ b/Control/Functor/Constrained.hs
@@ -90,16 +90,14 @@
 
   
 constrainedFmap :: (Category r, Category t, o a, o b, o (f a), o (f b)) 
-      => (        r a b               -> t (f a) (f b)                      ) 
-       -> ConstrainedCategory r o a b -> ConstrainedCategory t o (f a) (f b)
+      => (   r  a b ->    t  (f a) (f b)  ) 
+       -> (o⊢r) a b -> (o⊢t) (f a) (f b)
 constrainedFmap q = constrained . q . unconstrained
 
-instance (Functor [] k k, o [UnitObject k]) 
-       => Functor [] (ConstrainedCategory k o) (ConstrainedCategory k o) where
+instance (Functor [] k k, o [UnitObject k]) => Functor [] (o⊢k) (o⊢k) where
   fmap (ConstrainedMorphism f) = ConstrainedMorphism $ fmap f
 
-instance (o (), o [()], o Void, o [Void]) => SumToProduct []
-     (ConstrainedCategory (->) o) (ConstrainedCategory (->) o) where
+instance (o (), o [()], o Void, o [Void]) => SumToProduct [] (o⊢(->)) (o⊢(->)) where
   sum2product = ConstrainedMorphism sum2product
   mapEither (ConstrainedMorphism f) = ConstrainedMorphism $ mapEither f
   filter (ConstrainedMorphism f) = ConstrainedMorphism $ filter f
diff --git a/Data/Foldable/Constrained.hs b/Data/Foldable/Constrained.hs
--- a/Data/Foldable/Constrained.hs
+++ b/Data/Foldable/Constrained.hs
@@ -127,9 +127,8 @@
   ffoldl f (i,Just a) = f(i,a)
 
 
-instance ( Foldable f s t, WellPointed s, WellPointed t
-         , Functor f (ConstrainedCategory s o) (ConstrainedCategory t o) 
-         ) => Foldable f (ConstrainedCategory s o) (ConstrainedCategory t o) where
+instance ( Foldable f s t, WellPointed s, WellPointed t, Functor f (o⊢s) (o⊢t) )
+              => Foldable f (o⊢s) (o⊢t) where
   foldMap (ConstrainedMorphism f) = ConstrainedMorphism $ foldMap f
   ffoldl (ConstrainedMorphism f) = ConstrainedMorphism $ ffoldl f
 
diff --git a/Data/Traversable/Constrained.hs b/Data/Traversable/Constrained.hs
--- a/Data/Traversable/Constrained.hs
+++ b/Data/Traversable/Constrained.hs
@@ -91,11 +91,6 @@
    where mM Nothing = constPure Nothing `inCategoryOf` f $ mempty
          mM (Just x) = fmap (arr Just) . f $ x
 
--- data Stupid a = Stupid a
--- instance Functor Stupid (ConstrainedCategory (->) Num) (->) where
---   fmap (Stupid (ConstrainedMorphism f)) (Stupid a) = Stupid (f a)
--- 
-
 -- | Flipped version of 'traverse' / 'mapM'.
 forM :: forall s t k m a b l . 
         ( Traversable s t k l, Monoidal m k l, Function l
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.1.1
+Version:             0.4.0.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
@@ -44,6 +44,8 @@
                       , tagged
                       , void
                       , semigroups
+                      , contravariant
+                      , trivial-constraint >= 0.4 && < 0.5
   Default-Extensions: ConstraintKinds
                       TypeFamilies
                       FlexibleInstances