Locally Graded Categories #458
Conversation
| _≈ᵥ_ : ∀ {X Y X' Y'} {f : X ⇒₁ Y} → X' ⇒[ f ] Y' → X' ⇒[ f ] Y' → Set e' | ||
|
|
||
| -- Directed transport along 2-cells in the grading category. | ||
| _⟨_⟩ : ∀ {X Y X' Y'} {f g : X ⇒₁ Y} → X' ⇒[ g ] Y' → f ⇒₂ g → X' ⇒[ f ] Y' |
There was a problem hiding this comment.
why is this contravariant?
There was a problem hiding this comment.
I think of the transport as a sort of substitution operation, so it feels more natural to be contravariant. Also has the nice benefit of making the laws line up with the directions of the unitors/associators that you'd expect.
Ultimately doesn't matter too much though, as you can get the opposite variance by grading over co.
There was a problem hiding this comment.
I definitely see the laws lining up, which is nice. It just seems weird that f ⇒₂ g is used to transform a X' ⇒[ g ] Y' to a X' ⇒[ f ] Y'. That 2-cell might not be invertible. Calling it a "sort of substitution operation" only mildly helps.
| -- | ||
| -- Locally graded categories are a joint generalization of displayed categories | ||
| -- and enriched categories: display can be obtained by picking a discrete | ||
| -- bicategory as your gradition, and enrichment can be obtained by asking |
There was a problem hiding this comment.
gradition -> gradation
|
Glad to see someone who knows what they're doing (i.e. not me) doing this! Is it missing that |
|
Yes it absolutely is; haven't touched setoids for a minute obviously :) Also needs congruence lemmas everywhere. |
This PR adds a definition of locally graded categories which are probably the "correct" notion of displayed category in E-category theory. They avoid the normal transport hell that comes with displayed setoids by directly axiomatizing a sort of "directed transport" operation along a morphism in a bicategory, which allows for all of the displayed equations to be turned into simple fibrewise ones.