Definition of cartesian monoidal structure for categories with finite products.

[dylanbraithwaite]

Standard construction of the monoidal structure for categories with binary products and a terminal object. The proofs of coherence equations are pretty ugly -- I tried formatting them with equational reasoning syntax but I don't think that brings much clarity, as the intermediate types are mostly just permutations of compositions of projection maps.

[maxsnew]

I think we should move these supporting constructions to a place where they can be reused.

Also I'm happy to merge the manual proofs you've done here but I think this is also good motivation for implementing a cartesian category solver.

[dylanbraithwaite]

Also I'm happy to merge the manual proofs you've done here but I think this is also good motivation for implementing a cartesian category solver.

Yeah I thought the same while writing them, but didn't think my Agda-fu was as that level yet. But looking at the ordinary category solver it doesn't seem as daunting as I expected, so I'll maybe have a go at it in the future if noone takes it on sooner.

[maxsnew]

Ok just fix the import style and then it's good to merge

[maxsnew]

Looks like there's also a whitespace error to fix

[dylanbraithwaite]

Looks like there's also a whitespace error to fix

I guess it's that there's no trailing newline in the BinProducts file? I'll fix that now.

Should I squash the commits too @maxsnew ?

[maxsnew]

I guess it's that there's no trailing newline in the BinProducts file? I'll fix that now.

For future reference you can just run the fix-whitespace utility, you don't really need to understand what the issue is.