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. But of course there are lots of useful categories where the objects are much more specific, e.g. vector spaces with linear maps as morphisms. The obvious way to express this in Haskell is as type class constraints, and the ConstraintKinds extension allows quantifying over such object classes.

Like in Control.Category, "the category k" means actually k is the 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.

Quite a few categories (monoidal categories) will permit "products" of objects as objects again – in the Haskell sense those are tuples – allowing for "dyadic morphisms" (x,y) ~> r.

Together with a unique UnitObject, this makes for a monoidal structure, with a few natural isomorphisms. Ordinary tuples may not always be powerful enough to express the product objects; we avoid making a dedicated associated type for the sake of simplicity, but allow for an extra constraint to be imposed on objects prior to consideration of pair-building.

The name Cartesian is disputable: in category theory that would rather Imply cartesian closed category (which we represent with Curry). Monoidal would make sense, but we reserve that to Functors.

Use this constraint to ensure that a, b and (a,b) are all "fully valid" objects of your category (meaning, you can use them with the Cartesian combinators).

Analogous to ObjectPair: express that k b c be an exponential object representing the morphism.

Monoidal categories need not be based on a cartesian product. The relevant alternative is coproducts.

The dual notion to Cartesian replaces such products (pairs) with sums (Either), and unit '()' with void types.

Basically, the only thing that doesn't mirror Cartesian here is that we don't require CoMonoid (ZeroObject k). Comonoids do in principle make sense, but not from a Haskell viewpoint (every type is trivially a comonoid).

Haskell of course uses sum types, variants, most often without Either appearing. But variants are generally isomorphic to sums; the most important (sums of unit) are methods here.

Apart from the identity morphism, id, there are other morphisms that can basically be considered identies. For instance, in any cartesian category (where it makes sense to have tuples and unit () at all), it should be possible to switch between a and the isomorphic (a, ()). iso is the method for such "pseudo-identities", the most basic of which are required as methods of the Cartesian class.

Why it is necessary to make these morphisms explicit: they are needed for a couple of general-purpose category-theory methods, but even though they're normally trivial to define there is no uniform way to do so. For instance, for vector spaces, the baseis of (a, (b,c)) and ((a,b), c) are sure enough structurally equivalent, but not in the same way the spaces themselves are (sum vs. product types).

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 totally ordered data types (but with arbitrary functions; this does not require monotonicity or anything).

Cast a morphism to its equivalent in a more constrained category, provided it connects objects that actually satisfy the extra constraint.

"Unpack" a constrained morphism again (forgetful functor).

Note that you may often not need to do that; in particular morphisms that are actually Functions can just be applied to their objects with $ right away, no need to go back to Hask first.

A proxy value is a "general representation" of a category's values, i.e. global elements. This is useful to define certain morphisms (including ones that can't just "inherit" from '->' with arr) in ways other than point-free composition pipelines. Instead, you can write algebraic expressions much as if dealing with actual values of your category's objects, but using the proxy type which is restricted so any function defined as such a lambda-expression qualifies as a morphism of that category.

Analogue to asTypeOf, this does not actually do anything but can give the compiler type unification hints in a convenient manner.

Tagged type for values that depend on some choice of category, but not on some particular object / arrow therein.