BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Weak factorization systems for intensional type theory - Paige Nor
 th - DPMMS ( DPMMS)
DTSTART:20150512T131500Z
DTEND:20150512T141500Z
UID:TALK59128@talks.cam.ac.uk
CONTACT:Dr Ignacio Lopez Franco
DESCRIPTION:In their paper\, van den Berg and Garner [1] described algebra
 ic conditions\non an endofunctor of a category which enable it to represen
 t the identity\ntype in an interpretation of dependent type theory. In thi
 s talk\, I will\ndescribe the weak factorization systems that can give ris
 e to such an\nendofunctor\, thus characterizing the weak factorization sys
 tems that can\ninterpret intensional type theory. In fact\, they are exact
 ly those in which\n(1) every object is fibrant and (2) the left class of m
 aps is stable under\npullback along the right class. I will also talk abou
 t internal categories\nand presheaves in such a category\, and under which
  conditions they\nthemselves form a category that can interpret intensiona
 l type theory.\n\n[1] Benno van den Berg and Richard Garner\, “Topologic
 al and simplicial\nmodels of identity types\,” ACM Trans. Comput. Log. 1
 3.1 (2012)\, Art. 3\, 44.\n
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR