Displayed functor cleanup #493
Open
Conversation
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
Someone who will not be named was not thinking clearly when defining displayed functors, and defined vertical functors and displayed functors as separate records. We can unify these two notions and provide alternative compositions instead.
I've wrapped is-fibred-functor in a no-eta record: this results in better inference.
Unless we make Id ∘ Id definitionally equal to Id, we can't unify vertical composition of displayed functors with composition. This means that we still need to have a separate notion of vertical adjunction.
I removed Vertical-fibred-functor and Fibred-functor: these are mostly just syntactic noise, and will be best served by using some sort of wide sub-bicategory construction. However, this requires us to change comprehension categories a bit.
Changed pages
|
ncfavier
previously approved these changes
May 11, 2025
plt-amy
reviewed
May 11, 2025
plt-amy
reviewed
May 11, 2025
|
This dropped off my radar a bit, but have some other stuff is touching this part of the code. Is this good to merge? |
ncfavier
approved these changes
May 23, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Description
Working on fibred limits and some of the design for fibred functors was starting to annoy me. Not sure what I
was thinking when I first wrote this!
Checklist
Before submitting a merge request, please check the items below:
support/sort-imports.hs(ornix run --experimental-features nix-command -f . sort-imports).If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with
chore:.