BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Homotopy Type Theory in Lean - Floris van Doorn (Carnegie Mellon U
 niversity)
DTSTART:20170711T103000Z
DTEND:20170711T113000Z
UID:TALK73232@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Co-authors: Ulrik Buchholtz		(TU Darmstadt)\, Jakob von Raumer
 		(University of Nottingham)        We discuss the homotopy type theory li
 brary in the Lean proof assistant. The library is especially geared toward
  synthetic homotopy theory\, and contains many results in that area\, amon
 g which are the computation of <br><br>\, a formalization of Eilenberg-Mac
 Lane spaces and the adjunction of pointed maps and the smash product. We h
 ave a novel method of implementing higher inductive types (HITs)\, where w
 e only take two HITs as primitives and add their computation rules to the 
 kernel of Lean. We define all other HITs in terms of these two primitive o
 nes. Other features include the use of cubical methods\, a large algebraic
  hierarchy and category theory library. Related Linkshttps://github.com/le
 anprover/lean2/blob/master/hott/hott.md &nbsp\;- The Lean HoTT libraryhttp
 s://github.com/cmu-phil/Spectral &nbsp\;- The Spectral Sequences project
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR