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

[Hendrik Boom]

On Fri, Aug 15, 2025 at 01:59:38AM -0400, Andrew Polonsky 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].

I need to ask:  What is the identity extension lemma?

--hendrik