Abstract
Supervised by Hugo Herbelin. Cubical Type Theory provides a computational meaning to Voevodsky’s univalence axiom. It uses an abstract interval to characterize equality types. Our goal here is to report on our progress trying to build a variant of this theory in which an equality between types is by definition an equivalence. Our approach is to use equality types computed by induction on types, inspired by parametricity.
Type
