Dualizing category theory API

Stream: PR reviews

[Dagur Asgeirsson]

I've reviewed #14258 and #14171, which are both straightforward dualizations of existing API in the category theory library, and should be ready to merge

[Dagur Asgeirsson]

The next one in the Kan extension refactor is ready to go: #14261

(I hope it's ok to use this channel to notify maintainers about PRs that I've reviewed and think are ready to merge, I just don't want them to go unnoticed for long after the review)

[Johan Commelin]

Thanks a lot for the review! And yes, posting comments like this is very welcome and encouraged!

[Ruben Van de Velde]

There's only one risk, and that's that at one point you might be roped into becoming a reviewer :)

[Dagur Asgeirsson]

Nothing wrong with that :smiley:

[Dagur Asgeirsson]

#14236 should be ready to go