Cubical type theory (CTT) gives computational meaning to homotopy type theory by introducing novel reasoning principles for equality. We explore one such reasoning principle, Kan filling, from a practical point of view. First, we study how to algorithmically derive Kan fillings, giving rise to a tactic that can automatically resolve many equality problems in CTT. Second, we formalise discrete Morse theory, a crucial method in applied topology, for graphs in Cubical Agda, a theorem prover implementing CTT. With these case studies we hope to provide some empirical data to help us understand how best to deal with equality in intensional type theory.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
