BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Impredicative encodings in HoTT - Steve Awodey (Carnegie Mellon Un
 iversity)
DTSTART:20170711T080000Z
DTEND:20170711T090000Z
UID:TALK73230@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:We investigate the prospects for impredicative encodings of in
 ductive types (including higher inductive types) in HoTT.&nbsp\; It is wel
 l-known that encoding inductives using higher-order quantification provide
 s a potential theoretical and practical simplification of the system.&nbsp
 \; Using the further resources available in HoTT allows for a sharpening o
 f the familiar System F style impredicative encodings of inductive types\,
  but this begs the question of whether impredicativity is formally compati
 ble with univalence.&nbsp\; We give a realizability model using a combinat
 ion of topos-theoretic\, homotopical\, and recent cubical methods.&nbsp\; 
 Joint work with Jonas Frey and Pieter Hofstra.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR