In the abstract (http://fomus.weebly.com/abstracts.html)  I meant the theory of Altenkich, Capriotti and Kraus (http://arxiv.org/abs/1604.03799) or the logic-enriched type theory by Part and Lou (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)  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.