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:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Polynomial models of type theory - Tamara von Gleh
n (DPMMS)
DTSTART;TZID=Europe/London:20180706T140000
DTEND;TZID=Europe/London:20180706T150000
UID:TALK107959AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/107959
DESCRIPTION:Polynomials (also known as containers) represent d
atatypes which\, like polynomial functions\, can b
e expressed using sums and products. Extending thi
s analogy\, I will describe the category of polyno
mials in terms of sums and products for fibrations
. This category arises from a distributive law bet
ween the pseudomonad ‘freely adding’ indexed sums
to a fibration\, and its dual adding indexed produ
cts. A fibration with sums and products is essenti
ally the structure defining a categorical model of
dependent type theory. I will show how the proces
s of adding sums to such a fibration is an instanc
e of a general 'gluing' construction for building
new models from old ones. In particular we can obt
ain new models of type theory in categories of pol
ynomials. Finally\, I will explore the properties
of other type formers in these models\, and consid
er which logical principles are and are not preser
ved by the construction.
LOCATION:FW26
CONTACT:Victor Gomes
END:VEVENT
END:VCALENDAR