Re: [HoTT] A unifying cartesian cubical type theory

[Andrew Pitts <Andrew.Pitts@cl.cam.ac.uk>]

On Thu, 14 Feb 2019 at 19:05, Anders Mortberg <andersmortberg@gmail.com> 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).

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
<https://ncatlab.org/nlab/show/Dold+fibration>?

Andy

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