search

mikeshulman / Coq-HoTT

Homotopy type theory
http://homotopytypetheory.org/
Other
12 stars 4 forks source link

Generalising DComma to sections of categories #45

Open Alizter opened 4 years ago

Alizter commented 4 years ago

It is mentioned in ooCat.v that DComma could possible be generalised to act on sections of displayed categories. This could then be used to define what a transfor is in general. I tried messing around with defining such a thing on paper but couldn't get it to work. What do we have in mind here?

Alizter commented 4 years ago

Also it might help to drop laxity for the moment.

mikeshulman commented 4 years ago

I know how to do this but haven't written it down yet. The thing to generalize is not DComma but DInserter. The annoying thing is that it seems to require the displayed category to be an isofibration, since the morphisms in the inserter have to live in fibers over identity maps, but composing with those identity maps is only the identity up to equivalence, so we have to transport back across that equivalence. Unless there is some other sneaky trick that I've missed.

mikeshulman commented 4 years ago

Oh, I just had an idea for a sneaky trick... maybe the thing to do is define the dependent inserter relative to a given not-necessarily-identity transformation. That is, given a natural transformation mu : F $=> G for functors F, G : A -> B, a displayed category C : B -> Type, and lifts of F and G to F' and G' landing in C, define a displayed category over A whose points over a are morphisms F' a $-> G' a displayed over mu a. I think maybe that would enable the coinduction to go through without isofibrancy, and then we could specialize it to mu being the identity endotransformation of the identity functor to get general DInserters. Of course, it requires having transformations already.