Skip to content

[Merged by Bors] - feat: 2-commutative squares#6233

Closed
joelriou wants to merge 9 commits intomasterfrom
catcommsq
Closed

[Merged by Bors] - feat: 2-commutative squares#6233
joelriou wants to merge 9 commits intomasterfrom
catcommsq

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jul 29, 2023

This PR introduces the notion of 2-commutative squares of functors.


Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Jul 29, 2023
@TwoFX
Copy link
Copy Markdown
Member

TwoFX commented Jul 29, 2023

Oops, sorry, I just noticed that this doesn't have awaiting-review yet.

@TwoFX TwoFX added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jul 30, 2023
@joelriou joelriou added awaiting-review WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes. awaiting-review labels Jul 30, 2023
@joelriou joelriou added awaiting-review and removed WIP Work in progress labels Jul 31, 2023
Copy link
Copy Markdown
Member

@TwoFX TwoFX 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 r+

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 31, 2023
bors bot pushed a commit that referenced this pull request Jul 31, 2023
This PR introduces the notion of 2-commutative squares of functors.



Co-authored-by: Joël Riou <[email protected]>
@bors
Copy link
Copy Markdown

bors bot commented Jul 31, 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: 2-commutative squares [Merged by Bors] - feat: 2-commutative squares Jul 31, 2023
@bors bors bot closed this Jul 31, 2023
@bors bors bot deleted the catcommsq branch July 31, 2023 18:22
kim-em pushed a commit that referenced this pull request Aug 2, 2023
This PR introduces the notion of 2-commutative squares of functors.



Co-authored-by: Joël Riou <[email protected]>
kim-em pushed a commit that referenced this pull request Aug 14, 2023
This PR introduces the notion of 2-commutative squares of functors.



Co-authored-by: Joël Riou <[email protected]>
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. t-category-theory Category theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants