Re: [HoTT] Different notions of equality; terminology

[Andrew Polonsky <andrew....@gmail.com>]

On Mon, Jul 18, 2016 at 11:05 PM, Vladimir Voevodsky <vlad...@ias.edu> 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.

I mean that your system with two equalities promotes strict equality
of MLTT from definitional to the logical level.  It remains
"substitutional" but can be asserted in context.

It would be nice to have a few simple demonstrations of the uses of
this, without getting into simplicial types.

Andrew