agda
Locally Graded Categories
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.
Glad to see someone who knows what they're doing (i.e. not me) doing this!
Is it missing that _≈ᵥ_ is an equivalence relation?
Yes it absolutely is; haven't touched setoids for a minute obviously :) Also needs congruence lemmas everywhere.