[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Jon, I must have seen an early version of Per’s Nagel lecture somewhere. I definitely wasn’t at CMU in 2013. It looks like the thing I was looking for. I’ll try to cajole some young minds here at TYPES 2023 to formalize the lectures. With kind regards, Andrej > On 13 Jun 2023, at 15:50, Jon Sterling <[email protected]> wrote: > > 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!WXYpkNUV5tYJlVXuiZQI97C8hXEYZVcohkLYzo-pn_4VNL1D6ez6rV1xf8vsge4MN36Af4fD_ieivgawrmCzHwwZ5MXYlZ03oes$ > . 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, [email protected] > <mailto:[email protected]> 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
