BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Dependent type theory and the univalence axiom - Ian Orton
DTSTART:20181024T100000Z
DTEND:20181024T110000Z
UID:TALK113911@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:In this talk I will present an introduction to dependent type 
 theory\, covering dependent pairs and functions\, identity types and unive
 rses. I will talk about the use of type theory as a constructive foundatio
 n for mathematics and give some examples of encoding proofs using dependen
 t types. I will then introduce the univalence axiom\, which implies that e
 quivalent types are equal. I will show how univalence is incompatible with
  the principle that all proofs of equality are the same (uniqueness of ide
 ntity proofs) and how other principles\, such as function extensionally\, 
 follow from the univalence axiom. If time allows I will also cover other r
 elated topics\, such as higher inductive types\, synthetic homotopy theory
  or cubical type theory.
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR