BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Univalent Universes of Sets - Andrew Pitts (University of Cambridg
 e)
DTSTART:20181127T141500Z
DTEND:20181127T151500Z
UID:TALK112534@talks.cam.ac.uk
CONTACT:Tamara von Glehn
DESCRIPTION:Presheaf categories have been used to make models of univalent
  type\ntheory\, first in classical set theory and later (with the "CCHM" m
 odel\nof Coquand's group) in some form of constructive set theory. Here I\
 nconcentrate on intuitionistic ZF set theory with atoms (IZFA). Back in\n1
 980 it was noticed by Mike Fourman\, Dana Scott and others that if one\nwo
 rks in IZFA\, then it is possible to regard presheaves (over a given\ninde
 x category) just as sets. At the same time\, dependent type theory\nhas a 
 straightforward interpretation in set theory. Under this\ninterpretation\,
  what is needed for a universe of sets in IZFA to model\nunivalence? Since
  univalence is a property of identity\, to answer this\nquestion one first
  has to look at the set-theoretic version of\n(propositional) identity typ
 es. Restricting to identity types\ngenerated by an interval\, I will discu
 ss some simple axioms that\nsuffice for universes of IZFA sets to be univa
 lent and which\nincorporate set-theoretic versions of some observations of
  Lumsdaine\,\nShulman and others. 
LOCATION:MR4\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR