Commit 2024-02-09 20:27 1d066860

View on Github →

feat(CategoryTheory/Limits): pushouts in the category of sets (#9992) This PR studies pushouts in the category of types. Specific properties of the pushout when one of the morphisms is injective are obtained. This PR partly removes the reference to the issue : the HasPushouts (Type _) instance can now be found automatically, but not HasPullbacks.

Estimated changes