Dan Christensen

@avigad Did you maybe mean to tag @david-christiansen instead of me?

Can you explain more? 1. I would assume that the typeclass search should be very fast, since in every case where we would use this, the instance should be obvious....

> I've [...] tried to make progress on the cocommutative comonoids giving commutative monoid structures on the homs. Unfortunately, this doesn't follow formally It should be formal. If `X` is...

Even if it is not definitional that a comonoid in `C` is a monoid in `C^op`, I still suspect that going via this statement might be a better way to...

@Alizter At this point, I don't remember the status of everything in this PR. Skimming the above, I see lots of discussions that haven't been marked as resolved, so it...