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!