Skip to content

[Merged by Bors] - feat(CategoryTheory): two more versions of the Yoneda lemma#14295

Closed
TwoFX wants to merge 1 commit intomasterfrom
more-yoneda-lemmas
Closed

[Merged by Bors] - feat(CategoryTheory): two more versions of the Yoneda lemma#14295
TwoFX wants to merge 1 commit intomasterfrom
more-yoneda-lemmas

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Jun 30, 2024

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 30, 2024

PR summary 8465857fd7

Import changes

No significant changes to the import graph

Declarations diff

+ coyonedaCompYonedaObj
+ largeCurriedCoyonedaLemma
+ largeCurriedYonedaLemma
+ uliftFunctor_obj
+ yonedaOpCompYonedaObj

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@joelriou joelriou changed the title feat: two more versions of the Yoneda lemma feat(CategoryTheory): two more versions of the Yoneda lemma Jun 30, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 30, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024
@TwoFX
feat(CategoryTheory): two more versions of the Yoneda lemma (#14295)
8c938d7
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): two more versions of the Yoneda lemma [Merged by Bors] - feat(CategoryTheory): two more versions of the Yoneda lemma Jun 30, 2024
@mathlib-bors mathlib-bors bot closed this Jun 30, 2024
@mathlib-bors mathlib-bors bot deleted the more-yoneda-lemmas branch June 30, 2024 17:26
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@TwoFX @dagurtomas
feat(CategoryTheory): two more versions of the Yoneda lemma (#14295)
1daae7c
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@TwoFX @joelriou