-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(CategoryTheory/Limits): pushouts in the category of sets #9992
Conversation
I left a couple of trivial comments but I'm not assigning this PR to myself because I'm not an active user of the category theory part of the library. |
Thanks @urkud for your suggestions! |
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Thanks @jcommelin for the suggestions which I have all applied. |
intro x y z hxy hyz | ||
obtain _|⟨_, _, h⟩|s|_ := hxy | ||
· exact hyz | ||
· obtain z₁|z₂ := z |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can this step also be integrated into the rintro
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the suggestions! I have used rintro
for the hxy
variable, but not for z
because this would create 8 goals instead of 7.
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
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 #5752 : the `HasPushouts (Type _)` instance can now be found automatically, but not `HasPullbacks`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
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 #5752 : the `HasPushouts (Type _)` instance can now be found automatically, but not `HasPullbacks`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
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 #5752 : the `HasPushouts (Type _)` instance can now be found automatically, but not `HasPullbacks`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
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 #5752 : the
HasPushouts (Type _)
instance can now be found automatically, but notHasPullbacks
.