[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hasegawa gives such a definition in "Parametricity of extensionally collapsed term models of polymorphism and their categorical properties", see Def. 3.4 and 3.8(iii). The fact that the extensional collapse of the overall-initial model is the initial parametric model follows from functoriality of the extensional quotient construction. I don't know if anyone has verified this explicitly, but it seems quite clear from how the construction is described by Breazu-Tannen and Coquand in "Extensional models for polymorphism", section 4 . Best, Andrew On Thu, Aug 28, 2025 at 1:21 PM Michael Shulman <[email protected]> wrote: > What is the definition of a "parametric model"? And can you give a > reference for the statement that the "extensional" quotient of the > overall-initial model is the initial parametric model? > > On Wed, Aug 27, 2025 at 9:20 PM Andrew Polonsky <[email protected]> > wrote: > >> [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Put >> Top = \forall X. X -> X >> tt = /\X.\x:X.x : Top >> T(X) = (X -> Top) -> (Top -> Top) >> A1 = A2 = Top >> R \subset A1xA2 is =beta(eta) >> T(R) identifies \x.x, \xy.y, and \xy.tt. >> >> While I agree that the term "initial model" is most often applied to a >> term >> model with a syntactic notion of equality, in discussions of IEL there's a >> general implicature that you are interested in parametric models. And the >> initial such model is precisely the extensional quotient of the term >> model, >> for which IEL holds tautologically. (More precisely, it holds by the >> fundamental theorem of logical relations, the version for open terms that >> is verified in the proof of the theorem.) >> >> Best, >> Andrew >> >> >> On Wed, Aug 27, 2025 at 7:59 PM Ryan Wisnesky <[email protected]> wrote: >> >> > 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 >> > >> ****************************************** >> > >> >> > >> > >> >
