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.