BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On Proofs of Equality as Paths - Andy Pitts\, Computer Laboratory
DTSTART:20161007T130000Z
DTEND:20161007T140000Z
UID:TALK67483@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:In the Type Theoretic approach to mathematical foundations\, p
 roofs about properties of mathematical objects can have the same status as
  the objects themselves. In particular\, proofs of equality become mathema
 tical objects that can be studied.  The homotopical approach to Type Theor
 y views proofs of equality as paths\, possibly in an abstract sense. Takin
 g this view literally\, what is required of an interval-like object II in 
 order to give a model of Type Theory in which elements of identity types r
 eally are just functions on II? I will discuss this question and introduce
  a surprisingly simple theory of the interval that suffices to model  the 
 recent Coquand-Danielsson axiomatization of propositional identity types.\
 n\n(Joint work with Ian Orton.)
LOCATION:FW26
END:VEVENT
END:VCALENDAR