University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Reasoning with Kan fillings about Morse reductions

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Reasoning with Kan fillings about Morse reductions

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Clifford Allbutt Zoom - Subscribe to mailing list for link in person & via zoom

Other talks

Afternoon Break Market Failure, Organ Shortage, Pandemic and Climate Change: The Architecture of Cooperation Online Causal Inference Seminar External Seminar - Hilde Nelissen TBC Talk TBC Talk title TBC
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity