2 papers
cs.LO2022
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…
math.LO2021
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…