BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Polynomial models of type theory - Tamara von Glehn (DPMMS)
DTSTART:20180706T130000Z
DTEND:20180706T140000Z
UID:TALK107959@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Polynomials (also known as containers) represent datatypes whi
 ch\, like polynomial functions\, can be expressed using sums and products.
  Extending this analogy\, I will describe the category of polynomials in t
 erms of sums and products for fibrations. This category arises from a dist
 ributive law between the pseudomonad ‘freely adding’ indexed sums to a
  fibration\, and its dual adding indexed products. A fibration with sums a
 nd products is essentially the structure defining a categorical model of d
 ependent type theory. I will show how the process of adding sums to such a
  fibration is an instance of a general 'gluing' construction for building 
 new models from old ones. In particular we can obtain new models of type t
 heory in categories of polynomials. Finally\, I will explore the propertie
 s of other type formers in these models\, and consider which logical princ
 iples are and are not preserved by the construction.
LOCATION:FW26
END:VEVENT
END:VCALENDAR