Re: [HoTT] Different notions of equality; terminology

[Dimitris Tsementzis <dtse...@princeton.edu>]

[-- Attachment #1: Type: text/plain, Size: 1832 bytes --]

I think this is terminological. I understood Polonsky (and correct me if I’m wrong) as saying that something like the “exact equality” of HTS is a “substitutive equality” that exists at the object (or what he is calling “logical”) level and can therefore be reasoned about. (It is of course distinct from the judgmental equality of HTS which lies in the background.) 

So is the so-called exact equality of HTS an example of a “substitutive equality” for you? Or do you still call that “transportational” and reserve the name “substitutive” for meta-level equalities that can only be checked? (This is a terminological question.)

Dimitris

> On Jul 18, 2016, at 17:05, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> 
> 
>> On Jul 18, 2016, at 10:45 PM, Andrew Polonsky <andrew....@gmail.com <mailto: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. 
> 
> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 3407 bytes --]