BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The HoTT library in Coq - Bas Spitters (Aarhus Universitet)
DTSTART:20170707T100000Z
DTEND:20170707T103000Z
UID:TALK73341@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:We report on the development of the HoTT library\, a formaliza
 tion of homotopy type theory in the Coq proof assistant. It formalizes mos
 t of basic homotopy type theory\, including univalence\, higher inductive 
 types\, and significant amounts of synthetic homotopy theory\, as well as 
 category theory and modalities. The library has been used as a basis for s
 everal independent developments. We discuss the decisions that led to the 
 design of the library\, and we comment on the interaction of homotopy type
  theory with recently introduced features of Coq\, such as universe polymo
 rphism and private inductive types. <br><br>Andrej Bauer\, Jason Gross\, P
 eter LeFanu Lumsdaine\, Mike Shulman\, Matthieu Sozeau\, Bas Spitters\, Th
 e HoTT Library: A formalization of homotopy type theory in Coq (CPP17) pp.
  164-172\, 2017 10.1145/3018610.3018615<br><a target="_blank" rel="nofollo
 w" href="https://arxiv.org/abs/1610.04591">https://arxiv.org/abs/1610.0459
 1</a><br><br><br>
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR