[HoTT] Re: [Agda] Univalence via Agda's primTrustMe?

Michael Shulman shulman at sandiego.edu
Sat Jan 17 18:15:46 CET 2015


On Sat, Jan 17, 2015 at 8:56 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> Does univalence preserve the identity strictly in any of the models?

It certainly does in the groupoid model.  I'm not as sure about
others, but it seems possible that using some cofibration-ness one
could choose it in such a way.


More information about the Agda mailing list