[Merged by Bors] - feat(CategoryTheory): retracts of objects and morphisms#19233
[Merged by Bors] - feat(CategoryTheory): retracts of objects and morphisms#19233
Conversation
PR summary b3e23b6de7Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Thanks! |
Defines retracts of objects and morphisms, and basic API. Used in #19135. Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
Defines retracts of objects and morphisms, and basic API. Used in #19135.