BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cubical Type Theory - Ian Orton (University of Cambridge)
DTSTART:20160429T101500Z
DTEND:20160429T111500Z
UID:TALK66076@talks.cam.ac.uk
CONTACT:Ian Orton
DESCRIPTION:In homotopy type theory (HoTT) we interpret equalities as path
 s. What does this actually mean? What are paths and what can we do with th
 em? Cubical type theory [1] is a formal system that allows us to reason ab
 out paths by introducing an abstract interval object into the type theory.
  By adding extra structure we can show that these paths have all the usual
  properties of identity types and more. In particular they allow us to pro
 ve the principle of function extensionality\, something that most existing
  type theories are unable to do. Adding yet more structure allows us to ob
 tain a computational interpretation of Voevodsky's univalence axiom.\n\nIn
  this talk I will introduce cubical type theory in stages. Starting with "
 vanilla" dependent type theory (without identity types) I will follow a pa
 ttern of: adding something to the type theory\, explaining why we don't ha
 ve identity types yet and repeating until we do.\n\nSpecifically\, I will 
 show that by simply adding an interval object to dependent type theory we 
 get a notion of path satisfying many of the properties that we expect of i
 dentity types (e.g. reflexivity\, symmetry\, congruence). Then I will desc
 ribe some of the shortcomings of these paths (we cannot prove that they ar
 e transitive or derive a notion of transport) and introduce some additiona
 l structure to fix these problems. Finally I will explain why\, after all 
 this work\, we still don't quite have the identity types that we all know 
 and love\, and how we can fix this using an idea of Andrew Swan.\n\n[1] C.
  Cohen\, T. Coquand\, S. Huber\, and A. Mörtberg. Cubical type theory: a 
 constructive interpretation of the univalence axiom. Preprint\, December 2
 015.
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR