Time: 1:00 - 2:00pm Venue: ITL top floor (QMUL)
Title: Polynomial models of type theorySpeaker: Tamara von GlehnHost: Edmund Robinsonhttp://theory.eecs.qmul.ac.uk/seminars/
AbstractPolynomials (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.Directions, if coming from outside QMULQueen Mary is on Mile End Road, with nearest tube stations being Stepney Green (closest one to the seminars) and Mile End. The seminars are in the Informatics Teaching Laboratory, floor 2. As the building has card access, it is best to inform us that you will be coming (nikos.tzevelekos@qmul.ac.uk).