Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors #11405

Closed
yuma-mizuno wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors #11405

yuma-mizuno wants to merge 17 commits into from

Conversation

@yuma-mizuno
Copy link
Collaborator

@yuma-mizuno yuma-mizuno commented Jan 12, 2022 •
edited by github-actions bot
Loading

This PR defines a bicategory structure on the oplax functors between bicategories.

Open in Gitpod

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 12, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 28, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

leanprover-community-bot-assistant commented Jan 28, 2022

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 28, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 9, 2022
@yuma-mizuno yuma-mizuno added the awaiting-review The author would like community review of the PR label Feb 10, 2022
jcommelin
jcommelin approved these changes Feb 10, 2022
View reviewed changes
Copy link
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 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Feb 10, 2022
bors bot pushed a commit that referenced this pull request Feb 10, 2022
@yuma-mizuno
feat(category_theory/bicategory/functor_bicategory): bicategory struc…
c3d8782 
…ture on oplax functors (#11405)

This PR defines a bicategory structure on the oplax functors between bicategories.
@bors
Copy link

bors bot commented Feb 10, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors [Merged by Bors] - feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors Feb 10, 2022
@bors bors bot closed this Feb 10, 2022
@bors bors bot deleted the bicategory-functor-bicategory branch February 10, 2022 15:13
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

2 more reviewers

@alreadydone alreadydone alreadydone approved these changes

@jcommelin jcommelin jcommelin approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@yuma-mizuno @leanprover-community-bot-assistant @alreadydone @jcommelin