[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
