A type theory enjoys *parametricity* when its types and terms can be equipped with an action on relations. This action can be applied to "automatically" derive uniformity properties of terms constructed in the theory; for example, any transformation between functors definable in the theory is guaranteed to be natural. I'll suggest that such properties are especially exploitable in higher-dimensional type theory, where we often find ourselves in need of higher-dimensional coherence properties that are tedious or even infeasible to verify by hand.

Bernardy, Coquand, and Moulin's internally parametric type theory is a type theory in which parametricity, normally metatheoretic, is made accessible *within* the theory. I'll describe joint work with Robert Harper in which we replay their design on top of cubical type theory, creating a setting where we can use parametricity in higher-dimensional theorem-proving. On the way, I'll highlight the similarities between internal parametricity and cubical type theory. Finally, I'll introduce cohesive modalities to this theory—following a similar move by Nuyts, Vezzosi, and Devriese—to connect the results in this theory to the original cubical setting.