diff --git a/Control/Applicative/Constrained.hs b/Control/Applicative/Constrained.hs
--- a/Control/Applicative/Constrained.hs
+++ b/Control/Applicative/Constrained.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Applicative.Constrained
 -- Copyright   :  (c) 2013 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 {-# LANGUAGE ConstraintKinds              #-}
 {-# LANGUAGE TypeFamilies                 #-}
@@ -29,6 +29,7 @@
           ) where
 
 
+import Control.Category.Constrained
 import Control.Functor.Constrained
 import Control.Arrow.Constrained
 
@@ -36,7 +37,8 @@
 import qualified Control.Category.Hask as Hask
 
 
-class (Functor f r t, Cartesian r, Cartesian t) => Monoidal f r t where
+class (Functor f r t, Cartesian r, Cartesian t, Object t (f (UnitObject r)))
+               => Monoidal f r t where
   pureUnit :: UnitObject t `t` f (UnitObject r)
   fzipWith :: (ObjectPair r a b, Object r c, ObjectPair t (f a) (f b), Object t (f c))
               => r (a, b) c -> t (f a, f b) (f c)
@@ -91,8 +93,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
@@ -2,7 +2,7 @@
 -- Module      :  Control.Arrow.Constrained
 -- Copyright   :  (c) 2013 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 -- Haskell's 'Arr.Arrow's, going back to [Hughes 2000], combine multiple ideas from
 -- category theory:
@@ -33,6 +33,7 @@
 {-# LANGUAGE FunctionalDependencies       #-}
 {-# LANGUAGE TupleSections                #-}
 {-# LANGUAGE ScopedTypeVariables          #-}
+{-# LANGUAGE UnicodeSyntax                #-}
 {-# LANGUAGE FlexibleInstances            #-}
 {-# LANGUAGE FlexibleContexts             #-}
 {-# LANGUAGE UndecidableInstances         #-}
@@ -74,6 +75,7 @@
 import GHC.Exts (Constraint)
 import Data.Tagged
 import Data.Void
+import Data.CategoryObject.Product
 
 import Data.Coerce
 import Data.Type.Coercion
@@ -82,6 +84,8 @@
 
 import Control.Category.Discrete
 
+import qualified Data.Functor.Contravariant as Hask
+
 infixr 1 >>>, <<<
 infixr 3 &&&, ***
 
@@ -242,7 +246,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 +264,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 +309,99 @@
   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
+instance (Morphism k, Morphism l) => Morphism (k×l) where
+  (f:***:g) *** (h:***:i) = (f***h) :***: (g***i)
+instance (PreArrow k, PreArrow l) => PreArrow (k×l) where
+  (f:***:g) &&& (h:***:i) = (f&&&h) :***: (g&&&i)
+  terminal = terminal :***: terminal
+  fst = fst :***: fst
+  snd = snd :***: snd
+
+prodCatUnit :: ∀ k l . (WellPointed k, WellPointed l)
+      => Tagged ((k×l) (ProductCatObj (UnitObject k) (UnitObject l))
+                       (ProductCatObj (UnitObject k) (UnitObject l)))
+                (ProductCatObj (UnitObject k) (UnitObject l))
+prodCatUnit = Tagged $ ProductCatObj uk ul
+ where Tagged uk = unit :: Tagged (k (UnitObject k) (UnitObject k)) (UnitObject k)
+       Tagged ul = unit :: Tagged (l (UnitObject l) (UnitObject l)) (UnitObject l)
+
+instance (WellPointed k, WellPointed l) => WellPointed (k×l) where
+  type PointObject (k×l) o = (PointObject k (LFactor o), PointObject l (RFactor o))
+  unit = prodCatUnit
+  const c = const (lfactorProj c) :***: const (rfactorProj 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
@@ -2,17 +2,19 @@
 -- Module      :  Control.Category.Constrained
 -- Copyright   :  (c) 2013-2016 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 -- 
 -- The most basic category theory tools are included partly in this
 -- module, partly in "Control.Arrow.Constrained".
 
 {-# LANGUAGE ConstraintKinds              #-}
+{-# LANGUAGE PolyKinds                    #-}
 {-# LANGUAGE TypeFamilies                 #-}
 {-# LANGUAGE MultiParamTypeClasses        #-}
 {-# LANGUAGE FlexibleContexts             #-}
 {-# LANGUAGE RankNTypes                   #-}
+{-# LANGUAGE UnicodeSyntax                #-}
 {-# LANGUAGE AllowAmbiguousTypes          #-}
 {-# LANGUAGE TypeOperators                #-}
 {-# LANGUAGE ExplicitNamespaces           #-}
@@ -20,6 +22,7 @@
 #if __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE UndecidableSuperClasses      #-}
 #endif
+{-# LANGUAGE LambdaCase                   #-}
 
 module Control.Category.Constrained ( 
             -- * The category class
@@ -30,12 +33,17 @@
             -- * Monoidal with coproducts
           , type (+)()
           , CoCartesian (..), ObjectSum
+            -- * The standard function category
+          , type Hask
             -- * Isomorphisms
           , Isomorphic (..)
             -- * Constraining a category
           , ConstrainedCategory (ConstrainedMorphism)
+          , type (⊢)()
           , constrained, unconstrained
           , ConstrainedFunction
+            -- * Product categories
+          , ProductCategory(..), type (×)()
             -- * Global-element proxies
           , HasAgent (..)
           , genericAlg, genericAgentMap
@@ -51,9 +59,16 @@
 import Data.Tagged
 import Data.Monoid
 import Data.Void
+import Data.CategoryObject.Product
+#if MIN_VERSION_base(4,9,0)
+import Data.Kind (Type)
+#endif
 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
@@ -69,8 +84,12 @@
 --   /morphism type constructor/. From a mathematician's point of view this may
 --   seem a bit strange way to define the category, but it just turns out to
 --   be quite convenient for practical purposes.
-class Category k where
-  type Object k o :: Constraint
+#if MIN_VERSION_base(4,9,0)
+class Category (k :: κ -> κ -> Type) where
+#else
+class Category (k :: κ -> κ -> *) where
+#endif
+  type Object k (o :: κ) :: Constraint
   type Object k o = ()
   id :: Object k a => k a a
   (.) :: (Object k a, Object k b, Object k c) 
@@ -86,6 +105,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 +129,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 +153,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 +255,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 +275,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 +320,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 +367,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 +438,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)
                                                                      
@@ -421,3 +490,25 @@
 instance Category Coercion where
   id = Hask.id
   (.) = (Hask..)
+
+
+infixr 3 :***:
+
+data ProductCategory k l p q = k (LFactor p) (LFactor q) :***: l (RFactor p) (RFactor q)
+
+type (×) = ProductCategory
+
+instance (Category k, Category l) => Category (k×l) where
+  type Object (k×l) o = (IsProduct o, Object k (LFactor o), Object l (RFactor o))
+  id = id:***:id
+  (f:***:g) . (h:***:i) = (f.h):***:(g.i)
+
+instance (Cartesian k, Cartesian l) => Cartesian (k×l) where
+  type UnitObject (k×l) = ProductCatObj (UnitObject k) (UnitObject l)
+  type PairObjects (k×l) a b = ( PairObjects k (LFactor a) (LFactor b)
+                               , PairObjects l (RFactor a) (RFactor b) )
+  swap = swap :***: swap
+  attachUnit = attachUnit :***: attachUnit
+  detachUnit = detachUnit :***: detachUnit
+  regroup = regroup :***: regroup
+  regroup' = regroup' :***: regroup'
diff --git a/Control/Category/Constrained/Prelude.hs b/Control/Category/Constrained/Prelude.hs
--- a/Control/Category/Constrained/Prelude.hs
+++ b/Control/Category/Constrained/Prelude.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Category.Constrained.Prelude
 -- Copyright   :  (c) 2013 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 
 {-# LANGUAGE ConstraintKinds              #-}
@@ -23,7 +23,7 @@
                       , Functor(..), (<$>), Applicative(..), (<*>), Monad(..), (=<<), filter
                       , mapM, mapM_, sequence, sequence_
                       , Foldable, foldMap, fold, traverse_, concatMap
-                      , Traversable, traverse )
+                      , Traversable, traverse, MonadFail(..) )
 
 import Control.Category.Constrained hiding (ConstrainedMorphism)
 import Control.Functor.Constrained
diff --git a/Control/Category/Constrained/Reified.hs b/Control/Category/Constrained/Reified.hs
--- a/Control/Category/Constrained/Reified.hs
+++ b/Control/Category/Constrained/Reified.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Category.Constrained.Reified
 -- Copyright   :  (c) 2016 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 -- 
 -- GADTs that mirror the class hierarchy from 'Category' to (at the moment) 'Cartesian',
diff --git a/Control/Category/Constrained/Reified/PolyPattern.hs b/Control/Category/Constrained/Reified/PolyPattern.hs
--- a/Control/Category/Constrained/Reified/PolyPattern.hs
+++ b/Control/Category/Constrained/Reified/PolyPattern.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Category.Constrained.Reified.PolyPattern
 -- Copyright   :  (c) 2016 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 -- 
 -- Pattern synonyms which allow you to deconstruct the various types
diff --git a/Control/Category/Discrete.hs b/Control/Category/Discrete.hs
--- a/Control/Category/Discrete.hs
+++ b/Control/Category/Discrete.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Category.Discrete
 -- Copyright   :  (c) 2018 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 -- 
 {-# LANGUAGE GADTs                #-}
diff --git a/Control/Category/Hask.hs b/Control/Category/Hask.hs
--- a/Control/Category/Hask.hs
+++ b/Control/Category/Hask.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Category.Hask
 -- Copyright   :  (c) 2013 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 -- Re-exports of all the common category-theory inspired classes from the
 -- "base" package, i.e. basically endofunctors in the Hask category (with
diff --git a/Control/Functor/Constrained.hs b/Control/Functor/Constrained.hs
--- a/Control/Functor/Constrained.hs
+++ b/Control/Functor/Constrained.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Functor.Constrained
 -- Copyright   :  (c) 2014 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 
 {-# LANGUAGE ConstraintKinds              #-}
@@ -19,9 +19,8 @@
 
 
 module Control.Functor.Constrained
-   ( module Control.Category.Constrained
-     -- * Functors
-   , Functor(..)
+   ( -- * Functors
+     Functor(..)
    , (<$>)
    , constrainedFmap
      -- * [Co]product mapping
@@ -42,7 +41,7 @@
 import Control.Category.Discrete
 
 
-class ( Category r, Category t, Object t (f (UnitObject r)) )
+class ( Category r, Category t )
            => 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))
      => r a b -> t (f a) (f b)
@@ -90,16 +89,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) => 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 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/Control/Monad/Constrained.hs b/Control/Monad/Constrained.hs
--- a/Control/Monad/Constrained.hs
+++ b/Control/Monad/Constrained.hs
@@ -2,7 +2,7 @@
 -- Module      :  Control.Monad.Constrained
 -- Copyright   :  (c) 2013 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 {-# LANGUAGE ConstraintKinds              #-}
 {-# LANGUAGE TypeFamilies                 #-}
@@ -36,6 +36,7 @@
                                 ) where
 
 
+import Control.Category.Constrained
 import Control.Applicative.Constrained
 import Data.Foldable.Constrained
 import Data.Traversable.Constrained
@@ -43,11 +44,12 @@
 
 import Prelude hiding (
      id, const, fst, snd, (.), ($)
-   , Functor(..), Applicative(..), Monad(..), (=<<)
+   , Functor(..), Applicative(..), Monad(..), MonadFail(..), (=<<)
    , uncurry, curry, filter
    , mapM, mapM_, sequence, sequence_
    )
 import qualified Control.Category.Hask as Hask
+import qualified Control.Monad.Fail as HaskFail
 
 import Control.Arrow.Constrained
 
@@ -131,7 +133,8 @@
 class (MonadPlus m k) => MonadFail m k where
   fail :: (Object k (m a)) => k String (m a) 
 
-instance (Hask.MonadPlus m, Hask.Applicative m) => MonadFail m (->) where
+instance (Hask.MonadPlus m, Hask.Applicative m, HaskFail.MonadFail m) 
+          => MonadFail m (->) where
   fail = Hask.fail
   
 
diff --git a/Data/CategoryObject/Product.hs b/Data/CategoryObject/Product.hs
new file mode 100644
--- /dev/null
+++ b/Data/CategoryObject/Product.hs
@@ -0,0 +1,49 @@
+-- |
+-- Module      : Data.CategoryObject.Product
+-- Copyright   : (c) Justus Sagemüller 2021
+-- License     : GPL v3
+-- 
+-- Maintainer  : (@) jsag $ hvl.no
+-- Stability   : experimental
+-- Portability : portable
+-- 
+
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+
+module Data.CategoryObject.Product where
+    
+import Data.Semigroup
+import Data.Monoid hiding ((<>))
+
+data ProductCatObj a b = ProductCatObj a b
+
+type family LFactor t where
+  LFactor (ProductCatObj l r) = l
+  LFactor (a,b) = (LFactor a, LFactor b)
+
+type family RFactor t where
+  RFactor (ProductCatObj l r) = r
+  RFactor (a,b) = (RFactor a, RFactor b)
+
+class IsProduct t where
+  lfactorProj :: t -> LFactor t
+  rfactorProj :: t -> RFactor t
+
+instance IsProduct (ProductCatObj a b) where
+  lfactorProj (ProductCatObj x _) = x
+  rfactorProj (ProductCatObj _ y) = y
+
+instance (IsProduct a, IsProduct b) => IsProduct (a,b) where
+  lfactorProj (x,y) = (lfactorProj x, lfactorProj y)
+  rfactorProj (x,y) = (rfactorProj x, rfactorProj y)
+
+
+instance (Semigroup a, Semigroup b) => Semigroup (ProductCatObj a b) where
+  ProductCatObj x y <> ProductCatObj w z = ProductCatObj (x<>w) (y<>z)
+
+instance (Monoid a, Monoid b) => Monoid (ProductCatObj a b) where
+  mempty = ProductCatObj mempty mempty
+  mappend (ProductCatObj x y) (ProductCatObj w z)
+       = ProductCatObj (mappend x w) (mappend y z)
diff --git a/Data/Foldable/Constrained.hs b/Data/Foldable/Constrained.hs
--- a/Data/Foldable/Constrained.hs
+++ b/Data/Foldable/Constrained.hs
@@ -2,7 +2,7 @@
 -- Module      :  Data.Foldable.Constrained
 -- Copyright   :  (c) 2014 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 {-# LANGUAGE ConstraintKinds              #-}
 {-# LANGUAGE TypeFamilies                 #-}
@@ -19,8 +19,7 @@
 
 
 module Data.Foldable.Constrained
-           ( module Control.Category.Constrained 
-           , Foldable(..)
+           ( Foldable(..)
            , fold
            , traverse_, mapM_, forM_, sequence_
            , concatMap
@@ -127,9 +126,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
@@ -2,7 +2,7 @@
 -- Module      :  Data.Traversable.Constrained
 -- Copyright   :  (c) 2014 Justus Sagemüller
 -- License     :  GPL v3 (see COPYING)
--- Maintainer  :  (@) sagemueller $ geo.uni-koeln.de
+-- Maintainer  :  (@) jsag $ hvl.no
 -- 
 {-# LANGUAGE ConstraintKinds              #-}
 {-# LANGUAGE TypeFamilies                 #-}
@@ -19,8 +19,7 @@
 
 
 module Data.Traversable.Constrained
-           ( module Control.Applicative.Constrained 
-           , Traversable(..)
+           ( Traversable(..)
            , forM
            , EndoTraversable
            , haskTraverse
@@ -90,11 +89,6 @@
   traverse f = arr mM 
    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 . 
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.2.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
@@ -27,7 +27,7 @@
 License:             GPL-3
 License-file:        COPYING
 Author:              Justus Sagemüller
-Maintainer:          (@) sagemueller $ geo.uni-koeln.de
+Maintainer:          (@) jsag $ hvl.no
 Homepage:            https://github.com/leftaroundabout/constrained-categories
 Build-Type:          Simple
 Cabal-Version:       >=1.10
@@ -40,10 +40,13 @@
 
 Library
   Default-Language:   Haskell2010
-  Build-Depends:      base>=4.7 && <5
+  Build-Depends:      base>=4.8 && <5
                       , tagged
                       , void
                       , semigroups
+                      , contravariant
+                      , fail
+                      , trivial-constraint >= 0.4 && < 0.8
   Default-Extensions: ConstraintKinds
                       TypeFamilies
                       FlexibleInstances
@@ -61,4 +64,5 @@
                       Control.Category.Constrained.Reified.PolyPattern
                       Data.Foldable.Constrained
                       Data.Traversable.Constrained
+                      Data.CategoryObject.Product