BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:UniMath - its present and its future. - Vladimir Voevodsky (Instit
 ute for Advanced Study\, Princeton)
DTSTART:20170710T103000Z
DTEND:20170710T113000Z
UID:TALK73197@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:UniMath refers to several things. It is a<br>univalent foundat
 ion of mathematics. It is the subset of Coq in which this<br>foundation is
  currently implemented and it is a library of formalized<br>mathematics wr
 itten using this implementation. My talk will be mostly about the<br>libra
 ry. I will give examples of problems whose constructions have been<br>rece
 ntly formalized in the UniMath as study problems by graduate students. I<b
 r>will give an example of a more complex problem whose construction has be
 en<br>recently formalized as a part of a paper accepted to a conference pr
 oceedings.<br>Finally\, I will outline a direction for the future developm
 ent of the UniMath<br>that requires constructions to considerably more com
 plex problems that can only<br>be stated in the univalent type theory and\
 , as far as I know\, have never been<br>solved either formally or informal
 ly.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR