Dan, It is an interesting idea to refer to univalence as a “mechanism” rather than an “axiom”. Even if you did it for expository reasons, I believe that in certain contexts it is a good phrase to adopt. Dimitris > On Nov 7, 2017, at 16:40, Daniel R. Grayson wrote: > > See https://www.nature.com/articles/d41586-017-05477-9 > > -- > 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 HomotopyTypeThe...@googlegroups.com . > For more options, visit https://groups.google.com/d/optout .