limits in opposite categories

Stream: maths

[Chris Hughes]

What is the reason most of the lemmas about limits in opposite categories are not instances? For example, docs#category_theory.limits.has_pullbacks_opposite

[Johan Commelin]

Maybe it stems back from the time that those classes contained data?

[Bhavik Mehta]

I don't think so - it looks like these were added in May of this year

[Joël Riou]

Indeed, I added has_pullbacks_opposite quite recently. I did not make it an instance because the other similar lemmas about finite (co)limits, etc. were not instances either.

[Adam Topaz]

These are all props, so it should be safe to make them instances (at least one would hope!)

[Scott Morrison]

Resolved in #16511.