1

Parametricity and semi-cubical types
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 …
Hugo Moeneclaey
PDF Cite
Finitary higher inductive types in the groupoid model
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a …
Hugo Moeneclaey, Peter Dybjer
PDF Cite