Cocartesian and Bicartesian categories

Stream: Is there code for X?

[William Sørensen]

Hi i am formalizing the cambridge category theory course, and for this i wondered if there was a notion of bi-cartesian closed categories in mathlib?

[Aaron Liu]

we have docs#CategoryTheory.CartesianMonoidalCategory and docs#CategoryTheory.CartesianClosed but I don't see a typeclass for an explicit choice of finite coproducts

[Aaron Liu]

found the PR: #28718

[Aaron Liu]

until that lands maybe you can just get by with docs#CategoryTheory.Limits.HasFiniteCoproducts

[William Sørensen]

hmm i dont like this because theres no defeqs with it. I am thinking of just duplicating all of the work that has been done with the CMC and then defining a bicart cat from that. Unfortunate though

[Matt Diamond]

funny enough, the author of that PR (@Jad Ghalayini) just bumped this thread earlier today, seems kind of related?

#mathlib4 > to_additive on MonoidalCategory @ 💬

[William Sørensen]

Oh lol he’s literally right next door to me in my department. Thanks for this