[TYPES] Types-list Digest, Vol 155, Issue 3

[Michael Shulman]

Thanks for this answer, Andrew!

On Sat, Aug 16, 2025 at 9:17 AM Andrew Polonsky <andrew.polonsky at gmail.com>
wrote:

> 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].
>

No, that's not what we mean by "initial model".  In all my prior experience
in categorical logic and semantics of type theories, the "initial model"
has always referred to the quotient of closed terms (or more generally
terms in specified context) by the definitional equality of the theory
(usually something like beta-eta).  This is called the "initial model"
because it is the initial object of a category of suitably structured
categories (e.g. CCCs for STLC), which are the "models" of the type theory,
qua Generalized Algebraic Theory, in the usual sense of universal algebra.

I am also used to calling this the "syntactic category" or "term model",
but I discovered in talking to people who think about System F that to them
these phrases are ambiguous to them and might refer to something like the
extensional quotient that you mention since they are also "built out of
terms", so I switched to "initial model'.  Can this also be ambiguous?  Is
the extensional quotient also an initial object of a category of models?
What phrase should I use that is unambiguous to System F people?

So anyway, I think this is the answer we wanted:


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