BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Two-Level Type Theory - Nicolai Kraus (University of Nottingham)
DTSTART:20171107T141500Z
DTEND:20171107T151500Z
UID:TALK94090@talks.cam.ac.uk
CONTACT:Tamara von Glehn
DESCRIPTION:I give an introduction to *two-level type theory*\, a system t
 hat can combine two Martin-Lof style type theories.  We can take one of th
 em to be homotopy type theory (HoTT)\, and the other to be a version of ML
 TT with unique identity proofs.  This yields an extension of HoTT where a 
 "type of strict equalities" is available\, and from the point of view of H
 oTT\, this strict equality can be compared to judgmental/definitional equa
 lity\; essentially\, we get a variant of HoTT where it is possible to reas
 on internally about judgmental equality.\n  This system can be understood 
 as a variant of Voevodsky's *homotopy type system* (HTS).  Both HTS and tw
 o-level type theory address the issue that certain higher-categorical stru
 ctures cannot be suitably encoded in standard HoTT (cf. semisimplicial typ
 es).\n  Two-level type theory has been suggested by Altenkirch-Capriotti-K
  (arXiv:1604.03799 / CSL'16)\, developed further by Annenkov-Capriotti-K (
 arXiv:1705.03307)\, and a conservativity result has been shown by Capriott
 i (arXiv:1702.04912 / PhD thesis). 
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR