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…