The next 700 syntactical models of type theory

A family of syntactic models for the calculus of construction with universes ( CC ω ) is described, all of them preserving conversion of the calculus definitionally, and thus giving rise directly to a program transformation of CC ω into itself. Those models are based on the remark that negative type constructors (e.g. dependent product, coinductive types or universes) are underspecified in type theory-which leaves some freedom on extra intensional specifications. The model construction can be seen as a compilation phase from a complex type theory into a simpler type theory. Such models can be used to derive (the negative part of) independence results with respect to CC ω , such as functional extensionality, propositional extensionality, univalence or the fact that bisimulation on a coinductive type may not coincide with equality. They can also be used to add new principles to the theory, which we illustrate by defining a version of CC ω with ad-hoc polymorphism that shows in particular that parametricity is not an implicit requirement of type theory. The correctness of some of the models/program transformations have been checked in the Coq proof assistant and have been instrumented as a Coq plugin.