[TYPES] Identity extension for the system F term model

Wed Aug 27 23:34:34 EDT 2025

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
> >> ******************************************
> >>
>
>