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:Identity types in Algebraic Model Structures - And
rew Swan\, The Logic Group\, School of Mathematics
\, University of Leeds
DTSTART;TZID=Europe/London:20160212T140000
DTEND;TZID=Europe/London:20160212T150000
UID:TALK63137AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/63137
DESCRIPTION:The original Bezem-Coquand-Huber cubical set model
promised to give a constructive model of homotopy
type theory. However\, in its original form there
was a notable shortcoming: one of the definitiona
l equalities usually included in type theory\, the
J computation rule was absent. One way to fix thi
s is to use an alternative definition of identity
type in which we keep track more carefully of dege
nerate paths. The new identity type has a nice pre
sentation in the setting of algebraic model struct
ures. I'll use this idea to show that in particula
r cubical sets with Kan fibrations satisfy Garner
and van den Berg's notion of "homotopy theoretic m
odel of identity types." In this way we get a cons
tructive proof that cubical sets model intensional
type theory including all definitional equalities
.\n
LOCATION:FW11
CONTACT:Ohad Kammar
END:VEVENT
END:VCALENDAR