Skip to content

[Merged by Bors] - feat: quasi-isomorphisms are preserved by functors which preserve homology#7993

Closed
joelriou wants to merge 5 commits intomasterfrom
preserves_homology5
Closed

[Merged by Bors] - feat: quasi-isomorphisms are preserved by functors which preserve homology#7993
joelriou wants to merge 5 commits intomasterfrom
preserves_homology5

Conversation

@joelriou
Copy link
Copy Markdown
Contributor


Open in Gitpod

Copy link
Copy Markdown
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 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 30, 2023

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Oct 30, 2023
@joelriou
Copy link
Copy Markdown
Contributor Author

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 30, 2023
bors bot pushed a commit that referenced this pull request Oct 30, 2023
@bors
Copy link
Copy Markdown

bors bot commented Oct 30, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: quasi-isomorphisms are preserved by functors which preserve homology [Merged by Bors] - feat: quasi-isomorphisms are preserved by functors which preserve homology Oct 30, 2023
@bors bors bot closed this Oct 30, 2023
@bors bors bot deleted the preserves_homology5 branch October 30, 2023 20:20
grunweg pushed a commit that referenced this pull request Nov 1, 2023
fgdorais pushed a commit that referenced this pull request Nov 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants