Merged
Conversation
…void name clashes
…pective coequalizers
…cts by isomorphic one
…izers to the module
…cly after its definiton; common parameters are lifted to the module
Bring changes about coequalizers from the review process to the localcoequalizers branch
… the pre-existing on instead
…rd to speed-up type checking
JacquesCarette
requested changes
Jun 17, 2025
Collaborator
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
A few minor things - this is in excellent shape.
|
|
||
| module Categories.Bicategory.LocalCoequalizers {o ℓ e t} (𝒞 : Bicategory o ℓ e t) where | ||
|
|
||
| open import Categories.Diagram.Coequalizer |
Collaborator
There was a problem hiding this comment.
using clauses please
Contributor
Author
|
This is ready for re-review. |
JacquesCarette
approved these changes
Jun 23, 2025
Collaborator
|
Waiting for the CI to complete (had to resolve a merge conflict) and then will merge, assuming everything goes well. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This pull request contains the definition of a bicategory with local coequalizers (cf. Shulman - Framed Bicategories and Monoidal Fibrations, Ch. 11). This is part of a larger project constructing a bicategory of monads and bimodules.