Skip to content

[Merged by Bors] - feat(Condensed): the functor from TopCat to LightCondSet#13504

Closed
dagurtomas wants to merge 10 commits intomasterfrom
dagur/LightTopComparison
Closed

[Merged by Bors] - feat(Condensed): the functor from TopCat to LightCondSet#13504
dagurtomas wants to merge 10 commits intomasterfrom
dagur/LightTopComparison

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Jun 4, 2024 •
edited
Loading

@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory t-condensed Condensed mathematics labels Jun 4, 2024
@dagurtomas dagurtomas mentioned this pull request Jun 4, 2024
Closed
1 task
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 4, 2024
@ghost ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jun 4, 2024
@ghost ghost removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jun 6, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jun 7, 2024

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 7, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

No significant changes to the import graph

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 7, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 10, 2024 •
edited
Loading

PR summary 47ff0fbe99

Import changes

No significant changes to the import graph

Declarations diff

+ TopCat.toCondensedSet
+ TopCat.toLightCondSet
+ topCatToCondensedSet
+ topCatToLightCondSet
- TopCat.toCondensed
- topCatToCondensed

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>

kim-em
kim-em reviewed Jul 1, 2024
View reviewed changes
kim-em
kim-em reviewed Jul 1, 2024
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 1, 2024

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 1, 2024

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jul 1, 2024
@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Jul 1, 2024

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024
@dagurtomas
feat(Condensed): the functor from TopCat to LightCondSet (#13504)
e655d3b 
- [x] depends on: #13503
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Condensed): the functor from TopCat to LightCondSet [Merged by Bors] - feat(Condensed): the functor from TopCat to LightCondSet Jul 1, 2024
@mathlib-bors mathlib-bors bot closed this Jul 1, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/LightTopComparison branch July 1, 2024 21:15
dagurtomas added a commit that referenced this pull request Jul 2, 2024
@dagurtomas
feat(Condensed): the functor from TopCat to LightCondSet (#13504)
d3774bd 
- [x] depends on: #13503
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-category-theory Category theory t-condensed Condensed mathematics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@dagurtomas @kim-em