Post #1005991
2026-03-31 14:15 UTC
I've just added to my formalisation of @jemlord 's "Easy Parametricity" a short proof that every function of type (A : U) → A → A is the identity. Such a neat idea!
Replies (1)
-
@jemlord@mathstodon.xyz 2026-03-31 22:23
@ncf Yay, thank you! It's cool seeing it come together in a proof assistant.