BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The encode-decode method for equality types - Alex Rice (Universit
 y of Cambridge)
DTSTART:20220303T110000Z
DTEND:20220303T120000Z
UID:TALK171020@talks.cam.ac.uk
CONTACT:Alex Rice
DESCRIPTION:Identity types in Martin-Lof type theory are a powerful tool f
 or reasoning about programs and mathematics. While induction on this type 
 easily allows us to define lots of operations\, it can be harder to give a
  concrete characterisation of the identity type. The encode-decode method 
 is a generic technique for solving this problem.\n\nI will give a recap of
  the definition of the identity type\, describe the encode-decode method a
 nd give some examples of it on some basic types before giving a more invol
 ved example using univalence.
LOCATION: FW09 - William Gates Building
END:VEVENT
END:VCALENDAR