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 and Semantics Seminar (Computer Laboratory)
SUMMARY:On Proofs of Equality as Paths - Andy Pitts\, Comp
uter Laboratory
DTSTART;TZID=Europe/London:20161007T140000
DTEND;TZID=Europe/London:20161007T150000
UID:TALK67483AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/67483
DESCRIPTION:In the Type Theoretic approach to mathematical fou
ndations\, proofs about properties of mathematical
objects can have the same status as the objects t
hemselves. In particular\, proofs of equality beco
me mathematical objects that can be studied. The
homotopical approach to Type Theory views proofs o
f equality as paths\, possibly in an abstract sens
e. Taking this view literally\, what is required o
f an interval-like object II in order to give a mo
del of Type Theory in which elements of identity t
ypes really are just functions on II? I will discu
ss this question and introduce a surprisingly simp
le theory of the interval that suffices to model
the recent Coquand-Danielsson axiomatization of pr
opositional identity types.\n\n(Joint work with Ia
n Orton.)
LOCATION:FW26
CONTACT:Dominic Mulligan
END:VEVENT
END:VCALENDAR