[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks everyone for the informative discussion! Andrew’s counter-example of T(X) = X->X to the IEL in the initial model is just what was asked for. If I may ask a follow-up: does anyone have a counter-example for the IEL in the initial model for a type expression that defines a functor? Or a proof that IEL always holds for definable functors in the initial model? (T(X) = X->X is well-known not to be a functor.). Thanks again! Ryan > On Aug 14, 2025, at 10:59 PM, Andrew Polonsky <[email protected]> > wrote: > > [ 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 >> ****************************************** >>
