Zulip Chat Archive

Stream: lean4

Topic: Parametricity and Lean 4?


David Thrane Christiansen (Jun 26 2022 at 08:58):

Does anyone have pointers to literature on the current state of parametricity (in the sense of Reynolds) WRT Lean's type theory? I know there was a flurry of research on either proving parametricity properties for various flavors of dependent type theory, or adding tools to make it internally observable, but I don't really have a good overview of the current state of the field.

Mario Carneiro (Jun 26 2022 at 09:00):

It's generally false in lean because of the existence of classical.choice


Last updated: Dec 20 2023 at 11:08 UTC