diff --git a/Control/Applicative/Constrained.hs b/Control/Applicative/Constrained.hs
--- a/Control/Applicative/Constrained.hs
+++ b/Control/Applicative/Constrained.hs
@@ -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)
diff --git a/Control/Arrow/Constrained.hs b/Control/Arrow/Constrained.hs
--- a/Control/Arrow/Constrained.hs
+++ b/Control/Arrow/Constrained.hs
@@ -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
@@ -306,6 +308,27 @@
   globalElement = Hask.const
   unit = Hask.pure ()
   const = Hask.const
+
+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
diff --git a/Control/Category/Constrained.hs b/Control/Category/Constrained.hs
--- a/Control/Category/Constrained.hs
+++ b/Control/Category/Constrained.hs
@@ -42,6 +42,8 @@
           , type (⊢)()
           , constrained, unconstrained
           , ConstrainedFunction
+            -- * Product categories
+          , ProductCategory(..), type (×)()
             -- * Global-element proxies
           , HasAgent (..)
           , genericAlg, genericAgentMap
@@ -57,6 +59,7 @@
 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
@@ -487,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/Functor/Constrained.hs b/Control/Functor/Constrained.hs
--- a/Control/Functor/Constrained.hs
+++ b/Control/Functor/Constrained.hs
@@ -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)
@@ -94,10 +93,10 @@
        -> (o⊢r) a b -> (o⊢t) (f a) (f b)
 constrainedFmap q = constrained . q . unconstrained
 
-instance (Functor [] k k, o [UnitObject k]) => Functor [] (o⊢k) (o⊢k) 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 [] (o⊢(->)) (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
@@ -36,6 +36,7 @@
                                 ) where
 
 
+import Control.Category.Constrained
 import Control.Applicative.Constrained
 import Data.Foldable.Constrained
 import Data.Traversable.Constrained
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
@@ -19,8 +19,7 @@
 
 
 module Data.Foldable.Constrained
-           ( module Control.Category.Constrained 
-           , Foldable(..)
+           ( Foldable(..)
            , fold
            , traverse_, mapM_, forM_, sequence_
            , concatMap
diff --git a/Data/Traversable/Constrained.hs b/Data/Traversable/Constrained.hs
--- a/Data/Traversable/Constrained.hs
+++ b/Data/Traversable/Constrained.hs
@@ -19,8 +19,7 @@
 
 
 module Data.Traversable.Constrained
-           ( module Control.Applicative.Constrained 
-           , Traversable(..)
+           ( Traversable(..)
            , forM
            , EndoTraversable
            , haskTraverse
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.4.1.0
+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
@@ -46,7 +46,7 @@
                       , semigroups
                       , contravariant
                       , fail
-                      , trivial-constraint >= 0.4 && < 0.5
+                      , trivial-constraint >= 0.4 && < 0.8
   Default-Extensions: ConstraintKinds
                       TypeFamilies
                       FlexibleInstances
@@ -64,4 +64,5 @@
                       Control.Category.Constrained.Reified.PolyPattern
                       Data.Foldable.Constrained
                       Data.Traversable.Constrained
+                      Data.CategoryObject.Product