Skip to content
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(category_theory/limits): yoneda preserves limits #5439

Closed
wants to merge 3 commits into from

Conversation

b-mehta
Copy link
Collaborator

@b-mehta b-mehta commented Dec 19, 2020

yoneda and coyoneda preserve limits

@b-mehta b-mehta added the awaiting-review The author would like community review of the PR label Dec 19, 2020
@bryangingechen bryangingechen linked an issue Dec 19, 2020 that may be closed by this pull request
src/category_theory/limits/yoneda.lean Outdated Show resolved Hide resolved
src/category_theory/limits/yoneda.lean Outdated Show resolved Hide resolved
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 21, 2020
bors bot pushed a commit that referenced this pull request Dec 21, 2020
@bors
Copy link

bors bot commented Dec 21, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/limits): yoneda preserves limits [Merged by Bors] - feat(category_theory/limits): yoneda preserves limits Dec 21, 2020
@bors bors bot closed this Dec 21, 2020
@bors bors bot deleted the yoneda-limits branch December 21, 2020 10:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

prove that the yoneda embedding preserves limits
2 participants