BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Univalent type theory and modular formalisation of mathematics - T
 hierry Coquand (Göteborgs Universitet)
DTSTART:20170627T100000Z
DTEND:20170627T110000Z
UID:TALK73080@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:&nbsp\;In the first part of the talk\, I will try to compare t
 he way mathematical collectionsare represented in set theory\, simple type
  theory\, dependent type theory and finallyunivalent type theory. The main
  message is that the univalence axiom is a strongform of extensionality\, 
 and that extensionality axiom is important for modularisationof concepts a
 nd proofs. The goal of this part is to explain to people familiar to simpl
 etype theory why it might be interesting to extend this formalism with dep
 endent types&nbsp\;and the univalence axiom.&nbsp\;The second part will tr
 y to explain in what way we can see models of univalent typetheory as gene
 ralisations of R. Gandy&rsquo\;s relative consistency proof of the extensi
 onalityaxioms for simple type theory.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR