[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi All, I'm hoping the folks on this list can settle a question of folklore; myself and Mike Shulman and others have been discussing it on the applied category theory zulip channel but have yet to reach a conclusion: https://urldefense.com/v3/__https://categorytheory.zulipchat.com/*narrow/channel/229199-learning.3A-questions/topic/Continuations.2C.20parametricity.2C.20and.20polymorphism/with/528479188__;Iw!!IBzWLUs!Uf89Hb7uWjtbz4qUeFbMCVwfxkuye2lpB27Oi4vChhMV6yMPpA57jl2oZnBt3TaOOYa7UhjQTz16dPMUZoGtGubQesXT$ The question is whether the initial (term) model of system F (2nd order impredicative polymorphic lambda calculus) satisfies the "identity extension lemma", which is one of the primary lemmas characterizing (Reynolds) parametric models. To be clear, this question is about the initial (term) model of system of F, its initial model of contexts and substitutions. There are many places that state the system F term model should obey identity extension, for example, this remark by Andy Kovacs: https://urldefense.com/v3/__https://cs.stackexchange.com/questions/136359/rigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici/136373*136373__;Iw!!IBzWLUs!Uf89Hb7uWjtbz4qUeFbMCVwfxkuye2lpB27Oi4vChhMV6yMPpA57jl2oZnBt3TaOOYa7UhjQTz16dPMUZoGtGpQSw3Ii$ . However, neither myself nor Mike nor anyone on the zulip chat or anyone we’ve asked has been able to find a proof (or disproof). Anyway, do please let me know if you know of a clear proof or disproof of the identity extension lemma for the initial (term) model of system F! Thanks, Ryan Wisnesky PS Here's a statement from Mike about the exact definition of this question: Let C be the initial model of system F. Let R(C) be the relational model built from C, so its objects are objects of C equipped with a binary relation. There is a strict projection functor R(C) -> C, and since C is initial this projection has a section C -> R(C), which is "external parametricity". In a theory like System F that has type variables, a "model" includes information about types in a context of type variables, so external parametricity sends every type in context to a "relation in context". Do the relations-in-context resulting in this way from types of System F always map identity relations to identity relations?
