Finally, Voevodsky currently distinguishes between "substitutive" and "transportational" equalities. But in his system, both concepts are of the "logical" kind. The effect is therefore to promote "strict" equality to the logical level; so one can reason about it in the object logic, while retaining other properties like the conversion rule.
I am not sure what you mean by this. In fact, I emphasized that the only substitutional equality in MLTTs is the definitional equality that can not be postulated or proved, only checked.
Vladimir.
--
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.