In the abstract (http://fomus.weebly.com/abstracts.html <http://fomus.weebly.com/abstracts.html>)  I meant the theory of Altenkich, Capriotti and Kraus (http://arxiv.org/abs/1604.03799 <http://arxiv.org/abs/1604.03799>) or the logic-enriched type theory by Part and Lou (https://arxiv.org/abs/1506.04998 <https://arxiv.org/abs/1506.04998>).  One can also apply it to the possible theories with the second transportational equality of the form suggested at the end of my talk today.

In the HTS (https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf <https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf>)  there is still only one substitutional and one transportational equality but the substitutional one is, indeed, type-based and so can be reasoned about at the object level.

Vladimir.


> On Jul 18, 2016, at 11:18 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
> 
> I mean whatever system is implicitly referred to by the last sentence
> in the abstract of your talk.
> 
> On Mon, Jul 18, 2016 at 11:16 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> Referring to it at what point in the talk?
>> 
>>> On Jul 18, 2016, at 11:16 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
>>> 
>>> I assumed you were referring in your talk to HTS or some variant of it.
>>> 
>>> On Mon, Jul 18, 2016 at 11:15 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>>>> I still do not understand. What do you mean by my system?
>>>> 
>>>>> On Jul 18, 2016, at 11:13 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
>>>>> 
>>>>> 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
>>>>> 
>>>>> --
>>>>> 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.
>>>> 
>>