BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Reasoning with Kan fillings about Morse reductions - Maximilian Do
 ré (University of Oxford)
DTSTART:20241010T160000Z
DTEND:20241010T170000Z
UID:TALK222244@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:Cubical type theory (CTT) gives computational meaning to homot
 opy type theory by introducing novel reasoning principles for equality. We
  explore one such reasoning principle\, Kan filling\, from a practical poi
 nt of view. First\, we study how to algorithmically derive Kan fillings\, 
 giving rise to a tactic that can automatically resolve many equality probl
 ems in CTT. Second\, we formalise discrete Morse theory\, a crucial method
  in applied topology\, for graphs in Cubical Agda\, a theorem prover imple
 menting CTT. With these case studies we hope to provide some empirical dat
 a to help us understand how best to deal with equality in intensional type
  theory.\n\n\n=== Hybrid talk ===\n\nRecording: https://www.youtube.com/wa
 tch?v=bU8Z6htWYrg&t=1s
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR