Polynomial models of type theory

Add to your list(s) Download to your calendar using vCal

• Tamara von Glehn (DPMMS)
• Friday 06 July 2018, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Victor Gomes.

Polynomials (also known as containers) represent datatypes which, like polynomial functions, can be expressed using sums and products. Extending this analogy, I will describe the category of polynomials in terms of sums and products for fibrations. This category arises from a distributive law between the pseudomonad ‘freely adding’ indexed sums to a fibration, and its dual adding indexed products. A fibration with sums and products is essentially the structure defining a categorical model of dependent 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 theory in categories of polynomials. Finally, I will explore the properties of other type formers in these models, and consider which logical principles are and are not preserved by the construction.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.