[TYPES] Equivalence invariance for MLTT (reference request)

[Jon Sterling]

Dear Andrej,

I am not completely sure because it is a while since I had watched this, but I think this might be related to the topic of Per Martin-Löf's 2013 Earnest Nagel Lecture “Invariance Under Isomorphism and Definability”, which you can find here: https://urldefense.com/v3/__https://www.cmu.edu/dietrich/philosophy/events/nagel-lectures/past-lectures.html__;!!IBzWLUs!WbQ8Sxq9uOhc-H40-I8IgA8jFEsX9FK7kI0GWPnCsjWqEW3A9Thx7H15rSmUBZyHOvIZExnwb8TJrd9CE7zzeP2HWx8$ . But I don't recall if Per proves the exact theorem you want; it might be a little different, judging from the abstract.

Best,
Jon


On 12 Jun 2023, at 20:56, andrej.bauer at andrej.com wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> in preparation for my TYPES 2023 talk I realized I don’t actually know of anyone having proved the following about MLTT (Σ + Π + Id + Nat).
>
> EQUIVALENCE INVARIANCE: Let P be a well-formed type expression with a type meta-variable X. If A and B are closed type expressions and e : A ≃ B an equivalence between them, then the type of equivalences P[A/X] ≃ P[B/X] is inhabited.
>
> There are many possible variants, of course, and I’d be interested in learning about any results in this direction, especially ones that don’t throw in any axioms.
>
> I am vaguely remebering that it has been done for Church’s simple type theory, which actually sounds, well, simple. Does anyone know a reference?
>
> I think there might have been some work by Bob Harper & Dan Licata (https://urldefense.com/v3/__https://www.cs.cmu.edu/*drl/pubs/lh112tt/lh122tt-final.pdf__;fg!!IBzWLUs!Ww4XrFxjdSUVFGjTgD3MToleD85TRwLRGFIy_xjkQqvSw3nuqa9fWxMNxAWYPT5FyS0Rr9hCcWv8p05bA6Xc3ZdFibwiK0ulYns$ ), and another by Nicolas Tabareau & Matthieu Sozeau (https://urldefense.com/v3/__https://doi.org/10.1145/3236787__;!!IBzWLUs!Ww4XrFxjdSUVFGjTgD3MToleD85TRwLRGFIy_xjkQqvSw3nuqa9fWxMNxAWYPT5FyS0Rr9hCcWv8p05bA6Xc3ZdFibwin1ZSLzI$ ), which cuts thing off at the groupoid level. I am not even sure if they really prove an analogue of the principle stated above.
>
> But how about pure MLTT, has anyone done it?
>
> With kind regards,
>
> Andrej