On Thursday, February 14, 2019 at 3:06:29 PM UTC-5, Andrew= Pitts wrote:
On Thu, 14 Feb 20= 19 at 19:05, Anders Mortberg <andersm...@gmail.com> wrote:
> The key idea is to weaken the notion of fibration from the cartesi= an
> Kan operations com^r->s so that they are not strictly the ident= ity
> when r=3Ds. Instead we introduce weak cartesian Kan operations tha= t are
> only the identity function up to a path when r=3Ds.

I was interested to read this, because I too use =C2=A0that weakened fo= rm
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 =E2=80=94 so far unpublished, because I can't qu= ite see how
to get univalent universes to work (but seem frustratingly close to
it).

Very interesting that you also conside= red this form of weakened fibrations! I also thought a bit about basing thi= ngs 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 connection= s and reversals (potentially with Boolean structure) homogeneous compositio= n (hcomp^0->1) is equivalent to binary composition, but without this str= ucture 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 i= n the sense of BCH...

Anyway, the univalent un= iverses (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 adapta= tion 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 long= er.
=C2=A0

Anyway, what I wanted to say is that perhaps one should call= these
things "Dold fibrations" by analogy with the classic notion o= f Dold
fibration in topological spaces
<https:/= /ncatlab.org/nlab/show/Dold+fibration>?

Andy

Thanks for the pointer! I didn't k= now about them and will have to think a bit whether what we have could be s= een as a cubical variation of them.

--
<= div>Anders
=C2=A0

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_390_1830799272.1550245083753-- ------=_Part_389_1458641519.1550245083753--