On Jul 18, 2016, at 10:45 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

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.