Parametricity and Lean 4?

Stream: lean4

[David Thrane Christiansen]

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]

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