BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Homotopy Type Theory and Univalent Foundations of Mathematics II -
  Chris Kapulkin\, University of Pittsburgh
DTSTART:20110629T131500Z
DTEND:20110629T141500Z
UID:TALK31966@talks.cam.ac.uk
CONTACT:Nathan Bowler
DESCRIPTION:This series of talks is an introduction to Homotopy Type Theor
 y and the Univalent Foundations of Mathematics. This new area of research 
 develops a beautiful connection between algebraic topology (homotopy theor
 y) and theoretical computer science (type theory).\n\nThe second talk will
  serve an introduction to the Univalent Foundations. This program started 
 by Vladimir Voevodsky (IAS\, Princeton) provides new interesting foundatio
 ns of mathematics (based on type theory)\, naturally formalizing categoric
 al and higher-categorical thinking. The main purpose of this project is to
  have a language based on homotopy types (as opposed to sets) that would e
 nable one to easily prove results from homotopy theory using a proof assis
 tant such as Coq. This can be accomplished by adding the Univalence Axiom 
 to the standard set of rules of type theory. In the talk we will discuss t
 he Univalence Axiom together with some of its basic consequences\, higher 
 inductive types\, and a type theoretic proof of $\\pi_1 (S^1) = \\mathbb{Z
 }$.
LOCATION:MR13\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR