CoCartesian and BiCartesian Categories

[bolt12]

When working on #21 I figured that having CoCartesian Categories, hence coproducts and even BiCartesian Categories formalized it would be more elegant to express some of the fields and laws of Logic. However adding CoCartesian to Categorical.{Raw,Laws} isn't trivial due to name clashing. A couple of possible solutions are:

• Put Cartesian and CartesianClosed in a local module called Cartesian and create a second local module called CoCartesian as well.
• Obtain the CoCartesian formalization via dualization
• more?

[conal]

When working on #21 I figured that having CoCartesian Categories, hence coproducts and even BiCartesian Categories formalized it would be more elegant to express some of the fields and laws of Logic.

I’d love to hear more of your thoughts about Cocartesian and Logic. I suspect you’re right about Cocartesian helping formulate Logic, perhaps even replacing the Boolean and Logic classes altogether. I feel on much firmer ground with the genuinely categorical classes than with Boolean and Logic.

[bolt12]

So my thoughts are that with Cocartesian, Cartesian categories we can factor out what Logic is really made of and with Bicartesian we can factor out the relation between ∧ and ∨ . The tricky part might be xor but since that can be written in terms of ∧ and ∨ it is fine.

not is still missing from the equation... we can go various routes with this:

• Create a Logic record that depends on being BiCartesian that adds the missing vocabulary and laws that relate everything.
• I remember from my journey through *-autonomous categories and compact closed categories (i.e. categories that have the notion of dual/dualizable objects) that propositional-logic fitted the pattern but couldn't actually be proved in a constructive setting. IIUC electric circuits classical logic works because one can inspect the value of the current and whatnot, so it might be the case that we can get away with exploring this categorical constructions as well!
• Lattices and Boolean Algebra bundle that basically bundle all the vocabulary/laws in terms of abstract algebra constructions that are not category theoretical