3 papers
cs.LO2026
Automating Boundary Filling in Cubical Type Theories
Maximilian Doré, Evan Cavallo, Anders Mörtberg
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to rea…
cs.LO2026
Univalence without function extensionality
Evan Cavallo, Jonas Höfer
It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of t…
math.AT2025
Relative elegance and cartesian cubes with one connection
Evan Cavallo, Christian Sattler
We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian…