  Parametricity is a key metatheoretic property of type systems, which implies
strong uniformity & modularity properties of the structure of types within
systems possessing it. In recent years, various systems of dependent type
theory have emerged with the aim of expressing such parametric reasoning in
their internal logic, toward the end of solving various problems arising from
the complexity of higher-dimensional coherence conditions in type theory. This
paper presents a first step toward the unification, simplification, and
extension of these various methods for internalizing parametricity.
Specifically, I argue that there is an essentially modal aspect of
parametricity, which is intimately connected with the category-theoretic
concept of cohesion. On this basis, I describe a general categorical semantics
for modal parametricity, develop a corresponding framework of axioms (with
computational interpretations) in dependent type theory that can be used to
internally represent and reason about such parametricity, and show this in
practice by implementing these axioms in Agda and using them to verify
parametricity theorems therein. I then demonstrate the utility of these axioms
in managing the complexity of higher-dimensional coherence by deriving
induction principles for higher inductive types, and in closing, I sketch the
outlines of a more general synthetic theory of parametricity, with applications
in domains ranging from homotopy type theory to the analysis of program
modules.
