In general no. But their model is essentially syntactic and more or less complete. Or, to be more precise, I would expect it to--be more or less complete.V.On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com> wrote:On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vladimir@ias.edu> wrote:The question is about how you interpret this operation for the univalent universe. If there is an interpretation of such an operation then there is a way to define equivalences between types in an involutionary way.I don’t follow why this should be the case. This shows that there is some notion of equivalence *in the model* (i.e. constructed in the meta-theory) which is strictly involutive. But there is no reason that this notion need be definable in the syntax of the object theory, is there?–p.--
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.
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.