Abstract

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.