The next 700 syntactical models of type theory

International audienceA 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 extensional-ity, 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 para-metricity 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