COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Polynomial models of type theory

## Polynomial models of type theoryAdd 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)
- Computer Laboratory talks
- Computing and Mathematics
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsNuclear Symposia Seminars in Ageing Research Genetics Seminar Series## Other talksFull-field optical metrology Title: "Pulling out all the stops" - Immunotherapy-associated arthritis. The model-independent theory of (∞,1)-categories (2) Art speak Thirteen ways of looking at an equivariant stable category Coping with Mechanical Stress: Tissue dynamics in development and repair |