BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Univalent polymorphism - Benno van den Berg (University of Amsterd
 am)
DTSTART:20180130T141500Z
DTEND:20180130T151500Z
UID:TALK99751@talks.cam.ac.uk
CONTACT:Tamara von Glehn
DESCRIPTION:This talk will be concerned with Hyland’s effective topos. I
 t turns out that this topos is the homotopy category of an interesting pat
 h category (a path category is essentially a category of fibrant objects i
 n the sense of Brown in which every object is cofibrant). Within this path
  category one can identify an interesting subclass of the fibrations: the 
 discrete ones. This subclass contains a universal element\, which is\, how
 ever\, not univalent. By passing to a more complicated category\, one can 
 obtain a universe for discrete hsets which is univalent. These categories 
 provide weak models of the calculus of constructions plus univalent univer
 ses plus resizing (weak in the sense that many equalities hold up only in 
 propositional form).
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR