Reasoning with Kan fillings about Morse reductions

Add to your list(s) Download to your calendar using vCal

• Maximilian Doré (University of Oxford)
• Thursday 10 October 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Jonas Bayer.

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 ===

Recording: https://www.youtube.com/watch?v=bU8Z6htWYrg&t=1s

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.