BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:The HoTT library in Coq - Bas Spitters (Aarhus Uni
versitet)
DTSTART;TZID=Europe/London:20170707T110000
DTEND;TZID=Europe/London:20170707T113000
UID:TALK73341AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/73341
DESCRIPTION:We report on the development of the HoTT library\,
a formalization of homotopy type theory in the Co
q proof assistant. It formalizes most of basic hom
otopy type theory\, including univalence\, higher
inductive types\, and significant amounts of synth
etic homotopy theory\, as well as category theory
and modalities. The library has been used as a bas
is for several independent developments. We discus
s the decisions that led to the design of the libr
ary\, and we comment on the interaction of homotop
y type theory with recently introduced features of
Coq\, such as universe polymorphism and private i
nductive types.

Andrej Bauer\, Jason Gross
\, Peter LeFanu Lumsdaine\, Mike Shulman\, Matthie
u Sozeau\, Bas Spitters\, The HoTT Library: A form
alization of homotopy type theory in Coq (CPP17) p
p. 164-172\, 2017 10.1145/3018610.3018615

https://arxiv.org/abs/1610.0459
1

LOCATION:Seminar Room 2\, Newton Institute
CONTACT:INI IT
END:VEVENT
END:VCALENDAR