[TYPES] Equivalence invariance for MLTT (reference request)

[andrej.bauer at andrej.com]

Dear Steve,

thanks for the references. In my TYPES talk I  mentioned both Linedanbaum & Tarski and Per-Martin Löf (as well as your invariance property, but it doesn’t show up on the slides explicitly, I think, it’s in the speaker notes – I should publish the slides). At TYPES I learned about

“External univalence for second-order generalized algebraic theories”, Rafaël Bocquet, https://urldefense.com/v3/__https://arxiv.org/abs/2211.07487__;!!IBzWLUs!SDZI6H0UM7PuOlMIe9xtyo0Ao-iVwWXV_zlCW0pZLTtpCplwIWtfSAtRYm4gaYvcp1NYB37k4Cd_yy2_QjjOAgrmaRpWtKcbcds$ 

This work generalizes previous results, including Per-Martin Löf’s Nagel lecture.

With kind regards,

Andrej



> On 25 Jun 2023, at 08:09, Steve Awodey <awodey at andrew.cmu.edu> wrote:
> 
> Gents,
> 
> This invariance property was mentioned in my 2013 paper:
> 
> https://urldefense.com/v3/__https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf__;!!IBzWLUs!SDZI6H0UM7PuOlMIe9xtyo0Ao-iVwWXV_zlCW0pZLTtpCplwIWtfSAtRYm4gaYvcp1NYB37k4Cd_yy2_QjjOAgrmaRpWzXBAusg$ 
> 
> and is discussed in more detail in this one from 2018:
> 
> https://urldefense.com/v3/__https://www.andrew.cmu.edu/user/awodey/preprints/uapl.pdf__;!!IBzWLUs!SDZI6H0UM7PuOlMIe9xtyo0Ao-iVwWXV_zlCW0pZLTtpCplwIWtfSAtRYm4gaYvcp1NYB37k4Cd_yy2_QjjOAgrmaRpWk7t4cNs$ 
> 
> Invariance under equivalence in MLTT of course generalizes isomorphism invariance in *simple* type theory, 
> which was proved by Lindenbaum & Tarski in 1935.
> 
> Per’s 2013 Nagel Lecture at CMU was on a related but different topic, namely *relational invariance* —  i.e. “parametricity” — and essentially sketches a relational model of TT (a model in Set^G for the graph category G = * \rightrightarrows *).
> 
> In the papers cited above, I made the point that VV’s model of univalence implies that there cannot be a closed type \X.P(X) with X : U that’s *not* equivalence invariant, else given A ~ B and P(A) we would have both P(B) from univalence and transport, but not P(B), by assumption.  I think Peter L. observed that this semantic argument still admits the possibility that in MLTT w/o UA there exist closed terms
> 
> |- e : A ~ B
> |- a : P(A)
> 
> but no closed term 
> 
> |- b : P(B).
> 
> Of course, one can also give a direct syntactic proof of equivalence invariance by induction on the type structure - the cases of which are essentially done in Chapter 2 of the HoTT Book.
> 
> My (rhetorical) interest in this invariance property was Tarski's 1966 proposal to take isomorphism invariance of concepts in simple type theory as an explication of a “logical concept”, extending Felix Klein’s characterization of different geometric notions.  My point was that equivalence invariance in MLTT is an even wider relation than isomorphism invariance in STT, and thus detemines an even more general class of concepts that can be regarded as “logical”.  But perhaps they should instead be regarded as something even more general, such as "constructible”?
> 
> Best wishes,
> 
> Steve
> 
> 
>> On Jun 24, 2023, at 10:21 PM, types-list-request at lists.seas.upenn.edu <types-list-request at LISTS.SEAS.UPENN.EDU> wrote:
>> 
>> Message: 3
>> Date: Tue, 13 Jun 2023 15:50:07 +0200
>> From: Jon Sterling <jon at jonmsterling.com>
>> To: andrej.bauer at andrej.com
>> Cc: types-list at lists.seas.upenn.edu
>> Subject: Re: [TYPES] Equivalence invariance for MLTT (reference
>> request)
>> Message-ID: <29A74C31-6195-4567-AC86-89D70BF49A5B at jonmsterling.com>
>> Content-Type: text/plain; charset="UTF-8"
>> 
>> 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
>> 
>