BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Identity types in Algebraic Model Structures - Andrew Swan\, The L
 ogic Group\, School of Mathematics\, University of Leeds
DTSTART:20160212T140000Z
DTEND:20160212T150000Z
UID:TALK63137@talks.cam.ac.uk
CONTACT:Ohad Kammar
DESCRIPTION:The original Bezem-Coquand-Huber cubical set model promised to
  give a constructive model of homotopy type theory. However\, in its origi
 nal form there was a notable shortcoming: one of the definitional equaliti
 es usually included in type theory\, the J computation rule was absent. On
 e way to fix this is to use an alternative definition of identity type in 
 which we keep track more carefully of degenerate paths. The new identity t
 ype has a nice presentation in the setting of algebraic model structures. 
 I'll use this idea to show that in particular cubical sets with Kan fibrat
 ions satisfy Garner and van den Berg's notion of "homotopy theoretic model
  of identity types." In this way we get a constructive proof that cubical 
 sets model intensional type theory including all definitional equalities.\
 n
LOCATION:FW11
END:VEVENT
END:VCALENDAR