Notions of parametricity as monoidal models for type theory

Hugo Moeneclaey

This article gives a solid theoretical grounding to the observation that cubical structures arise naturally when working with parametricity. We claim that cubical models are cofree…