Displayed categories

[Taneb]

• [x] Displayed categories
• [x] Total categories
• [x] Displayed setoid reasoning and displayed morphism reasoning
• [x] Displayed functors (defined locally but would be improved by displayed morphism reasoning)
• [x] Displayed natural transformations
• [x] Investigate displayed category of displayed categories#
• [ ] Vertical displayed functors
• [ ] Vertical displayed natural transformations?
• [ ] Category of displayed categories over a fixed base

[JacquesCarette]

I've done some work already based on your gist... see my Categorical Playground repo where your code is in Categorical/Displayed and mine in 2Level/Category.

Note that I'm not suggesting that my approach in 2Level/Category is 'right', it is very much an experiment that I'm in the middle of. But there might be things in there that could trigger an idea for you.

[Taneb]

One thing I've noticed doing this, I care a lot more about the exact proof that two morphisms are equal than I normally would. This meant it matters, and is a little unfortunate, that equational reasoning syntax has an extraneous trans refl at the end. I don't know if this is fixable but it's definitely possible to work around it.

I've also been trying to make sure that little things that I'm building on top of have the "right" proofs ("right" is very subjective here). For example, defining some things in Categories.NaturalTransformation so that they don't use sym as much when they could use sym-assoc instead.

[TOTBWF]

Yeah, I was somewhat worried about this. In the 1Lab we define (pre)categories to have an hSet of morphisms, which means that we can ignore any sort of coherence issues involved with equalities of equalities. In general, agda-categories is really working with the theory of wild (2,1)-categories; normally we just perform a sneaky version of truncation by dropping equality proofs, but this is going to cause some pretty serious problems as this work continues.

As a concrete example, cartesian morphisms are going to be really problematic. The universal property requires that a morphism be displayed over a composite, which often involves some amount of transport. This comes up when defining the factorization system on a fibration; you end up using the fact that every morphism f' : Hom[ f ] x y is also displayed over f . id.

[Taneb]

Composition of vertical functors is the first place I've hit where I've not been able to see a way around that we may have lots of different equalities between two functions. In particular, identity′ wants a F′.₁′ (G′.₁′ C.id′) E.≈[ refl ] E.id′ but I can only see how to get a F′.₁′ (G′.₁′ C.id′) E.≈[ trans refl refl ] E.id′.

[JacquesCarette]

Two things come to mind when I see this problem over things "over" equalities:

1. you're not being weak enough somewhere to that you are demanding a very particular proof instead of any proof
2. things are not strict enough, i.e. trans doesn't compute on refl.

Obviously these two things pull in polar opposite directions! I'd like to see more details as I'm stumbling in the dark a bit here. (And I'm super interested, as I think the same problem may well surface for both Multicategory and Double category.)

Influenced by the above, I would speculate that there are two needs for these proofs: we need them to be there so that things 'line up' properly, and we need them to 'properly exist' for well-definedness.

[TOTBWF]

Another perspective on this is that E-categories are sort of like half of a bicategory: we've got the 2-dimensional data of a bicategory, yet none of the equations or coherences.

Also, I'm pretty convinced that we need more than a type-family of morphisms: we need a setoid-family of morphisms!

If you have coherences, equations, and transport, then you might be able to work your way out of this jam.

[JacquesCarette]

I agree that E-categories are very much like bicategories with some of the coherences missing. What's so remarkable is how pretty much all of 1-category theory goes through!

Yes, some amount of transport is one way out of this jam. I'm quite curious to see if there are other ways around the problem. [There might not be - but I also thought that the current approach to agda-categories would fail miserably in the first 2 weeks of us porting the old code, and yet here we are...]

[TOTBWF]

I'm very interested in this as well; even in settings where you do have transport, it tends to be pretty miserable in practice. (This is especially true in cubical, where transport does not compute on refl)

I see two ways forward on this: the first involves some co-yoneda trickery; instead of having displayed morphisms living directly over some f, you define a type like

record Over (f : Hom x y) (x' : Ob[ x ]) (y : Ob[ y ]) : Type where
  field
    base : Hom x y
    over : f ≈ base
    hom : Hom[ base ] x' y'

and then only work in terms of Over. It's pretty heavy-weight, but should work.

The other approach is to treat things like having fibre categories as honest-to-god structure. This is pretty interesting in its own right, though I'll admit I haven't thought too deeply on it.

[TOTBWF]

As another addendum: there is a second perspective on E-categories, which is that they are wild categories. FWIW, this makes agda-categories even more miraculous; it's really surprising that you can keep truncating and things keep working out!

[JacquesCarette]

I prefer the "maximally unsaturated" point of view of Peter LeFanu Lumsdaine and Erik Palmgren (i.e. I think the concept is Palmgren's but I learned it from Peter). Unfortunately the slides seem to have disappeared from the Internet per se, but still available in various archives / caches. But I think the video https://youtu.be/glC8tC7xdBY is still available.

But on Over: I agree that if f ≈ g then Hom[ f ] x' y' and Hom[ g ] x' y' should be equivalent (as types). And this dependency should not itself depend on the choice of proof of f ≈ g .