Adds Algebra.Morphism.Construct.DirectProduct

[carlostome]

This PR adds proofs that projections from the product type are structure preserving maps (morphisms) from the direct product construction.

This not complete whatsoever, but at least it gives an initial template that can be extended over time.

[JacquesCarette]

looks good to me

[jamesmckinna]

Hmm: some things to maybe (re) consider

• names?
• tighter imports
• module organisation, including the inlining of the IsRelHomomorphism definitions, seems sub-optimal (see below)
• the interesting morphism, namely into the product object, isn't defined, not a deal breaker but defining it might expose further some of the issues above?

Suggested refactoring:

• add Relation.Binary.Morphism.Construct.Product first (to handle the IsRel* substrate, and factor out the dependency on the 'bare' Data.Product.Base structure) (PR incoming unless you pick this up) UPDATED: see [ add ] product structure on RawSetoid #2720
• slice the module structure you have orthogonally: so that eg. a module Proj₁ (refl : Reflexive M._≈_) where defines the various versions of proj₁ for each of the algebraic categories... etc. (WIP)

[MatthewDaggitt]

And I also agree with @jamesmckinna's suggestion that the actual morphism should be listed explicitly.

[MatthewDaggitt]

By convention in the library these should be named proj₁-isMagmaHomomorphism

[jamesmckinna]

#2720 offers alternative (sub-)module organisation, where each proj₁-isXHomomorphism could be defined as the IsXHomomorphism of a Proj₁ module, etc. as suggested above?

[jamesmckinna]

• level polymorphism
• suggest refactor in the light of [ add ] product structure on RawSetoid #2720

[carlostome]

I've tried to address the comments above.

However, I can't understand how the suggestion in:

• slice the module structure you have orthogonally: so that eg. a module Proj₁ (refl : Reflexive M._≈_) where defines the various versions of proj₁ for each of the algebraic categories... etc. (WIP)

would work. By this I mean, that the argument (refl : Reflexive M._≈_) already depends on a chosen algebraic structure
M, and thus it does not make sense to define the "various versions" of functions under such module.

I already rebased this branch on top of (a squashed version of) jamesmckinna:rel-product (see #2720) to have access to "relational homomorphisms".

[jamesmckinna]

Thanks @carlostome yes I think you're right that my suggestion about restructuring the module organisation was wrong.
That said, I'd be tempted to replay the 'export' trick from Relation.Binary.Morphism.Construct.Product to make your definitions in Algebra.Morphism.Construct.DirectProduct a bit less unwieldy, both to define, and to deploy?