BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &\; Semantics for Dummies
SUMMARY:Cubical Type Theory - Ian Orton (University of Cam
bridge)
DTSTART;TZID=Europe/London:20160429T111500
DTEND;TZID=Europe/London:20160429T121500
UID:TALK66076AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/66076
DESCRIPTION:In homotopy type theory (HoTT) we interpret equali
ties as paths. What does this actually mean? What
are paths and what can we do with them? Cubical ty
pe theory [1] is a formal system that allows us to
reason about paths by introducing an abstract int
erval object into the type theory. By adding extra
structure we can show that these paths have all t
he usual properties of identity types and more. In
particular they allow us to prove the principle o
f function extensionality\, something that most ex
isting type theories are unable to do. Adding yet
more structure allows us to obtain a computational
interpretation of Voevodsky's univalence axiom.\n
\nIn this talk I will introduce cubical type theor
y in stages. Starting with "vanilla" dependent typ
e theory (without identity types) I will follow a
pattern of: adding something to the type theory\,
explaining why we don't have identity types yet an
d repeating until we do.\n\nSpecifically\, I will
show that by simply adding an interval object to d
ependent type theory we get a notion of path satis
fying many of the properties that we expect of ide
ntity types (e.g. reflexivity\, symmetry\, congrue
nce). Then I will describe some of the shortcoming
s of these paths (we cannot prove that they are tr
ansitive or derive a notion of transport) and intr
oduce some additional structure to fix these probl
ems. Finally I will explain why\, after all this w
ork\, we still don't quite have the identity types
that we all know and love\, and how we can fix th
is 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 2015.
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
CONTACT:Ian Orton
END:VEVENT
END:VCALENDAR