On Thursday, February 14, 2019 at 3:06:29 PM UTC-5, Andrew Pitts wrote: > > On Thu, 14 Feb 2019 at 19:05, Anders Mortberg > wrote: > > The key idea is to weaken the notion of fibration from the cartesian > > Kan operations com^r->s so that they are not strictly the identity > > when r=s. Instead we introduce weak cartesian Kan operations that are > > only the identity function up to a path when r=s. > > I was interested to read this, because I too use that weakened form > of fibration in some work attempting to get a model of univalence > based only on composition of paths rather than more general Kan > filling operations — so far unpublished, because I can't quite see how > to get univalent universes to work (but seem frustratingly close to > it). > > Very interesting that you also considered this form of weakened fibrations! I also thought a bit about basing things on a binary composition operation, but I never could get it to work. I managed to convince myself some year ago that in the presence of connections and reversals (potentially with Boolean structure) homogeneous composition (hcomp^0->1) is equivalent to binary composition, but without this structure on the interval I don't really see what to do. But on the other hand, if you don't have connections then I don't think you need the fibrations to lift against arbitrary subtubes but rather only open boxes in the sense of BCH... Anyway, the univalent universes (in particular fibrancy of Glue types) is by far the hardest thing in our note (as seems to always be the case). The way we do it is an adaptation of what we did back in CCHM, but because of the weakness we have to do additional corrections in the construction which makes it quite a bit longer. Anyway, what I wanted to say is that perhaps one should call these > things "Dold fibrations" by analogy with the classic notion of Dold > fibration in topological spaces > ? > > Andy > Thanks for the pointer! I didn't know about them and will have to think a bit whether what we have could be seen as a cubical variation of them. -- Anders -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.