[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
[ 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
