Composable cartesian homomorphism properties

[conal]

Despite considerable effort, I have not yet succeeded in defining the cartesian or cocartesian counterparts to the composable homomorphism building blocks.

Cartesian.Sub is the cartesian counterpart to Category.Sub, which a variation of Categories.Category.SubCategory, refactored to enable SubCat intersection. (The issue there was sharing an object mapping U. An earlier attempt added an equality constraint argument to intersection, which was incompatible with a pretty binary infix notation.)

Category.Homomorphisms contains building blocks for the SubCat in Category.Sub. Each building block wraps up the homomorphism property for a single operation (nullary, unary, or binary), to be combined via the intersection and mapping operations defined in Category.Sub. [Category.Homomorphisms] only supports subcategories of Setoids, which I consider a weakness.

Cartesian.Homomorphisms is a start on the cartesian counterpart to Category.Homomorphisms. I got tangled up in types for the categorical ⊤ and _×_. In all of the uses I anticipate, the categorical ⊤ and _×_ will match in the underlying cartesian category (of which we’re forming a subcategory). I tried to state this assumption in the Ops structure in Cartesian.Sub but have been unable to exploit it successfully in Cartesian.Homomorphisms.

[conal]

@JacquesCarette: As you’ve expressed interest in helping, maybe a good first step would be for you to review Category.Sub, Category.Homomorphism, and Cartesian.Sub and discuss here in this issue. You may have some suggestions for improvements, and the discussion may help see how to approach the cartesian homomorphisms and beyond (including cocartesian, preadditive, and biproduct).