Hugo Herbelin- Investigations into Cubical Type Theory

Explore a lecture on investigations into cubical type theory presented by Hugo Herbelin at the Hausdorff Center for Mathematics. Delve into a work-in-progress variant of cubical type theory based on several key principles. Examine how equality is primitively attached to types and defined as equivalence for types themselves. Learn about type coercion through projection of equivalence proofs and the addition of a generic transverse level of dependent abstraction over a formal interval. Discover the inclusion of a primitive notion of strictly associative composition of equality proofs and its implications. Consider how this theory may be justified through an iterated parametricity translation to type theory with identity type. Gain insights into cutting-edge research in type theory during this hour-long presentation, part of the Hausdorff Trimester Program on Types, Sets and Constructions.