Abstract
We report on our investigations linking parametricity and cubical structures. Our slogan is that cubical models of type theory are cofreely parametric.
Using various notions of parametricity and of models of type theory, we will present the following as cofreely parametric.
* Categories with Families (CwF) of semi-cubical types, with Pi-types and a universe.
* Categories of cubical object, for any kind of cubes.
* CwF of setoids (here seen as 1-dimensional Kan objects), with a univalent universe of propositions.
* Clans of Reedy fibrant objects (work in progress).
* Tribes of Kan cubical objects (work in progress).
We will introduce a notion called interpretation, used to build these cofree objects.
Date
Oct 21, 2021
Location
HoTTEST
