Skip to content

[Merged by Bors] - feat: functors which commute with shifts#4429

Closed
joelriou wants to merge 5 commits intomasterfrom
commshift
Closed

[Merged by Bors] - feat: functors which commute with shifts#4429
joelriou wants to merge 5 commits intomasterfrom
commshift

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented May 28, 2023

This PR defines the notion of a functor which commutes with shifts, when both the source and target categories are equipped with shifts by a monoid.


Open in Gitpod

@jcommelin
Copy link
Copy Markdown
Member

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 2, 2023
bors bot pushed a commit that referenced this pull request Jun 2, 2023
This PR defines the notion of a functor which commutes with shifts, when both the source and target categories are equipped with shifts by a monoid.



Co-authored-by: Johan Commelin <[email protected]>
@bors
Copy link
Copy Markdown

bors bot commented Jun 2, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jun 2, 2023
This PR defines the notion of a functor which commutes with shifts, when both the source and target categories are equipped with shifts by a monoid.



Co-authored-by: Johan Commelin <[email protected]>
@bors
Copy link
Copy Markdown

bors bot commented Jun 2, 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: functors which commute with shifts [Merged by Bors] - feat: functors which commute with shifts Jun 2, 2023
@bors bors bot closed this Jun 2, 2023
@bors bors bot deleted the commshift branch June 2, 2023 11:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants