[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Yes, the initial model of System F satisfies the identity extension lemma, assuming that by "initial model" you mean the extensional quotient of closed terms as treated e.g. by Hasegawa [1]. The identity relation in this model is the extensional equality defined by induction on type structure with the usual logical relation conditions. This identifies terms that are not beta(-eta) convertible, like the two successors on the polymorphic church numerals. Nat = \forall A. (A -> A) -> (A -> A) S, S' : Nat -> Nat S = \nfs.f(nfs) S' = \nfs.nf(fs) If by "initial model" you mean something intensional like a lambda algebra with beta conversion, then IEL fails. We can use the same type as the counterexample. T(X) = X -> X A1 = A2 = Nat R \subset A1xA2 is =beta T(R) identifies S and S' Best, Andrew P.S. Regarding the other question raised in the Zulip chat you linked, whether every type A is isomorphic to "forall X. (A -> X) -> X" in this extensional model, I believe the answer to be "yes" based on comments by Thierry Coquand in [2], slide 52. [1] https://urldefense.com/v3/__https://doi.org/10.1007/3-540-54415-1_61__;!!IBzWLUs!S8aJh356wvmDdcHzuNn_x-n_pAINEuB9OorQS4vpVVPxzpk6f1Frz6bXU2iKOmWU2eJnfiof4UvCQ7Pz7EY2e8iQYns02p8_gTB7LQ$ [2] https://urldefense.com/v3/__https://youtu.be/6Ao9zXwyteY?si=5FdC5t5Mnyajmchz&t=4660__;!!IBzWLUs!S8aJh356wvmDdcHzuNn_x-n_pAINEuB9OorQS4vpVVPxzpk6f1Frz6bXU2iKOmWU2eJnfiof4UvCQ7Pz7EY2e8iQYns02p8az4OKSg$ On Tue, Aug 12, 2025 at 12:02 PM <[email protected]> wrote: > Send Types-list mailing list submissions to > [email protected] > > To subscribe or unsubscribe via the World Wide Web, visit > https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list > or, via email, send a message with subject or body 'help' to > [email protected] > > You can reach the person managing the list at > [email protected] > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Types-list digest..." > > > Today's Topics: > > 1. Identity extension for the system F term model (Ryan Wisnesky) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 11 Aug 2025 21:25:19 -0700 > From: Ryan Wisnesky <[email protected]> > To: "[email protected]" > <[email protected]> > Subject: [TYPES] Identity extension for the system F term model > Message-ID: <[email protected]> > Content-Type: text/plain; charset=utf-8 > > 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? > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Types-list mailing list > [email protected] > https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list > > > ------------------------------ > > End of Types-list Digest, Vol 155, Issue 3 > ****************************************** >
