Clean up monoidal functor properties

[jacquescomeaux]

I was intending to improve typechecking time, but I think I ended up making more progress on the "lines of Haskell compiled to" metric.

The biggest improvements came from moving equational proofs out of records fields and into where blocks, but I also noticed that some of my changes (not sure which) to make the proofs more readable also reduced the size of the Haskell.

So far Categories.Functor.Monoidal.Properties is down from 242362 lines of Haskell to 95295 lines. I'm not quite done updating that file yet. I plan to update Categories.Functor.Monoidal.Construction.Product as part of this PR as well.

I also added opposite braided and symmetric monoidal categorites, and an op field to the bundled forms. This does make accessing the op of the underlying category ever so slightly harder.

I changed the definition of flip-bifunctor for better definitional equality, and added a way to get the oplax structure of a strong monoidal functor.

[JacquesCarette]

Will review 'soon' - first have to fix the broken CI. So there will be a delay.

[JacquesCarette]

(closing and reopening to get the CI to run)

[jacquescomeaux]

Upon further inspection, Categories.Functor.Monoidal.Construction.Product does have equational proofs in record fields, but it doesn't seem particularly offensive in terms of lines of haskell, typechecking time, or readability. So I think I'll leave that one as it is for now, possibly to revisit in a future PR.

[Taneb]

I'm fairly sure that the issue isn't with proofs in record fields (directly), but with proofs used as arguments to functions to construct morphisms (e.g. various limits' universal), because these terms tend to be duplicated many times (for example in subsequent morphism reasoning proofs). Being in a record field isn't enough insulation against this.

[JacquesCarette]

There are issues with nameless proofs. First, usability: goals become giant. Second, because Agda is fairly eager to delta and eta expand, some record fields do end up duplicated. So more 'modern' agda-categories style tries to minimize proofs inline to record fields.

BTW, I've warmed up to co-patterns, so in some cases, I would be fine using those instead of records, if it feels more ergonomic to do so.

[JacquesCarette]

There's a conflict now - could you resolve it please?

[jacquescomeaux]

Will update this soon. Do copatterns provide "enough insulation"? Or do the proofs still need to be extracted and given a name and type signature when using copatterns?

[JacquesCarette]

I believe that co-patterns expand quite a lot less than explicit records. Definitely worth experimenting with -- but not worth major refactoring.