Cubical Syntax for Reflection-Free Extensional Equality

Jonathan Sterling, Carlo Angiuli, Daniel Gratzer

We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function exte…