Abstract
A parametric model of type theory is defined as a model where any type comes with a relation and any term respects these. Intuitively, this means that terms treat their inputs uniformly.
In recent years many cubical models of type theory have been proposed, often built to support some form of parametricity. In this thesis, we explain this phenomena by defending that cubical models of type theory are cofreely parametric. To do this, we define notions of parametricity and their associated parametric models, then we prove that cofreely parametric models exist, and finally we give examples of cubical models which are indeed cofreely parametric.
In Chapter 1, we define the standard parametricity in details for categories and clans, with homotopically-flavored examples of parametric models. Then we give an informal survey of variants of parametricity, giving us ample potential applications for the next chapters. An important variant is internal parametricity where any type comes with a reflexive relation.
In Chapter 2, we axiomatize the situation by going back to the historical approach to parametricity, namely that it is inductively proven for the initial model. So an extension by section of a theory is defined as an extension by inductively defined unary operations. This is made precise using signatures for quotient inductive-inductive types. The extensions of the theory of categories, clans and categories with families by the standard parametricity are all key examples of extensions by section. We prove that the forgetful functors coming from such extensions have right adjoints, so that cofreely parametric models exist. We also explain how to extend the standard parametricity to arrow types and universes.
In Chapter 3 we give an alternative axiomatization of parametricity, that manages to give a very compact description for cofreely parametric models when applicable. We work with a symmetric monoidal closed category V of models of type theory. We define a notion of parametricity as a monoid in V, and a parametric model as a module. Then we build cofreely (and freely) parametric models as coinduced (and induced) modules. We prove that strict variants of both the category of left exact categories and the category of clans are symmetric mon- oidal closed. Then we prove that both the lex categories of n-truncated cubical objects and the clans of Reedy fibrant cubical objects are cofreely parametric models for suitable notions of parametricity.
