Showing cs.LOShow all
2 papers · 1 filter
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…