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--