BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Homotopy type theory and algebraic weak factorization systems - Ni
 cola Gambino (University of Leeds)
DTSTART:20170131T141500Z
DTEND:20170131T151500Z
UID:TALK70601@talks.cam.ac.uk
CONTACT:Tamara von Glehn
DESCRIPTION:The theory of weak factorisation systems and Quillen model str
 uctures provides a very convenient setting to construct and analyze models
  of Homotopy Type Theory\, most notably the simplicial model defined by Vo
 evodsky\, in which types are interpreted as Kan fibrations.\n\nThe aim of 
 this talk is to explain how the theory of algebraic weak factorization sys
 tems provides an analogous understanding of the cubical model of Homotopy 
 Type Theory defined by Coquand and his collaborators\, in which types are 
 interpreted as uniform Kan fibrations\, i.e. fibrations equipped with a su
 itably coherent choice of diagonal fillers.  This involves the development
  of a general method to construct algebraic which satisfy the so-called Fr
 obenius property\, and leads to a new proof of the right properness of the
  model structure for Kan complexes.\n\nThe talk is based on joint work wit
 h Christian Sattler (Leeds).\n
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR