The authors consider the idea of treating a parametrized type as an arbitrary functor from some parametrizing category to a category of types, and giving elements semantics as natural transformations. They show that under reasonable hypotheses this is only possible when the parametrizing category is a groupoid. This suggests a semantics for a semiparametric form of polymorphism. They discuss the interpretation of this form of parametricity in a PER model, and show that it coincides with the ostensibly stronger form derived from dinaturality.
展开▼
