BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Category Theory Seminar
SUMMARY:Univalent Universes of Sets - Andrew Pitts (Univer
sity of Cambridge)
DTSTART;TZID=Europe/London:20181127T141500
DTEND;TZID=Europe/London:20181127T151500
UID:TALK112534AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/112534
DESCRIPTION:Presheaf categories have been used to make models
of univalent type\ntheory\, first in classical set
theory and later (with the "CCHM" model\nof Coqua
nd's group) in some form of constructive set theor
y. Here I\nconcentrate on intuitionistic ZF set th
eory with atoms (IZFA). Back in\n1980 it was notic
ed by Mike Fourman\, Dana Scott and others that if
one\nworks in IZFA\, then it is possible to regar
d presheaves (over a given\nindex category) just a
s sets. At the same time\, dependent type theory\n
has a straightforward interpretation in set theory
. Under this\ninterpretation\, what is needed for
a universe of sets in IZFA to model\nunivalence? S
ince univalence is a property of identity\, to ans
wer this\nquestion one first has to look at the se
t-theoretic version of\n(propositional) identity t
ypes. Restricting to identity types\ngenerated by
an interval\, I will discuss some simple axioms th
at\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
CONTACT:Tamara von Glehn
END:VEVENT
END:VCALENDAR