WhatarethoseclassextensionsfortheCartesianclassfor?

The Cartesian class from the constrained-category project is for categories, products of objects in which are objects in the same category yet again.

I wonder about the classes Cartesian extends:

class ( Category k                                      {- 1 -}
      , Monoid (UnitObject k)                           {- 2 -}
      , Object k (UnitObject k)                         {- 3 -}
      -- , PairObject k (UnitObject k) (UnitObject k)   {- 4 -}
      -- , Object k (UnitObject k,UnitObject k)         {- 5 -}
      ) => Cartesian k where
...

Points 1 and 3 are pretty straightforward:

• 1: Cartesian extends Category.
• 3: The UnitObject k shall indeed be an object in k.

Other points confuse me:

• 2: Why do we want UnitObject k to be a Monoid? A proper unit is indeed a monoid (() <> () = () and mempty = (); the same goes for all other units as there exists only one unit modula the isomorphisms like unitType2Id ~() = id), but it is a necessary condition, not a sufficient one. Why don't we implement some class like:

  class ProperUnit u where
      toUnitType :: u -> ()
      fromUnitType :: () -> u
  

  With the following law: fromUnitType . toUnitType = id.
  I reckon extending neither Monoid, nor the ProperUnit classes to add extra features to the code, simply making it more idiomatic. Or am I wrong?

• 4: This one is commented out. Why so? What did we need the pair of two units for in the first place? Isn't it as good as a regular unit? They are clearly isomorphic.

• 5: This one is commented out once again. Why so? And why did we need such a pair to be an object in the category? Isn't this condition weaker than the previous one?¹ The PairObject type institutes extra restrictions concerning pairs. If such a pair is, in fact, an object in the category, it still doesn't necessarily satisfy the PairObject restriction, in which case we can't use it at all.

Can someone, please explain the logic behind these 3 points.

¹ As Bartosz Milewski pointed out, PairObject (currently renamed into PairObjects) and ObjectPair are different restrictions, the latter being more strict, guaranteeing that we make up pairs of actual "tensorable" objects in a category, where such a pair exists as an object. In fact, points 1, 3, 4 and 5 are equivalent to ObjectPair k (UnitObject k) (UnitObject k). Still, I do not quite understand why we entertain such a condition (leaving it commented out).