Parametricity and Semi-Cubical Types

Hugo Moeneclaey

We construct a model of type theory enjoying parametricity from an arbitrary one. A type in the new model is a semi-cubical type in the old one, illustrating the correspondence bet…