[TYPES] Identity extension for the system F term model

Thu Aug 28 17:55:27 EDT 2025

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 <shulman at sandiego.edu>
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 <andrew.polonsky at gmail.com>
> 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 <wisnesky at gmail.com> 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 <
>> andrew.polonsky at gmail.com>
>> > 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 <
>> > types-list-request at lists.seas.upenn.edu>
>> > > wrote:
>> > >
>> > >> Send Types-list mailing list submissions to
>> > >>        types-list at LISTS.SEAS.UPENN.EDU
>> > >>
>> > >> 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
>> > >>        types-list-request at LISTS.SEAS.UPENN.EDU
>> > >>
>> > >> You can reach the person managing the list at
>> > >>        types-list-owner at LISTS.SEAS.UPENN.EDU
>> > >>
>> > >> 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 <wisnesky at gmail.com>
>> > >> To: "types-list at lists.seas.upenn.edu"
>> > >>        <types-list at LISTS.SEAS.UPENN.EDU>
>> > >> Subject: [TYPES] Identity extension for the system F term model
>> > >> Message-ID: <CC3F8356-0B05-4A68-9E87-DD181A587DB4 at gmail.com>
>> > >> 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
>> > >> Types-list at LISTS.SEAS.UPENN.EDU
>> > >> https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list 
>> > >>
>> > >>
>> > >> ------------------------------
>> > >>
>> > >> End of Types-list Digest, Vol 155, Issue 3
>> > >> ******************************************
>> > >>
>> >
>> >
>>
>