2026-09-24T13:48:05Zhttps://api.repository.cam.ac.uk/server/oai/request

oai:www.repository.cam.ac.uk:1810/2543942024-06-26T13:50:20Zcom_1810_213747com_1810_256064col_1810_213748

Polynomials and models of type theory 10.17863/CAM.16245 von Glehn, Tamara This thesis studies the structure of categories of polynomials, the diagrams that represent polynomial functors. Specifically, we construct new models of intensional dependent type theory based on these categories. Firstly, we formalize the conceptual viewpoint that polynomials are built out of sums and products. Polynomial functors make sense in a category when there exist pseudomonads freely adding indexed sums and products to fibrations over the category, and a category of polynomials is obtained by adding sums to the opposite of the codomain fibration. A fibration with sums and products is essentially the structure defining a categorical model of dependent type theory. For such a model the base category of the fibration should also be identified with the fibre over the terminal object. Since adding sums does not preserve this property, we are led to consider a general method for building new models of type theory from old ones, by first performing a fibrewise construction and then extending the base. Applying this method to the polynomial construction, we show that given a fibration with sufficient structure modelling type theory, there is a new model in a category of polynomials. The key result is establishing that although the base category is not locally cartesian closed, this model has dependent product types. Finally, we investigate the properties of identity types in this model, and consider the link with functional interpretations in logic. University of Cambridge 2015-06-30 Thesis Doctoral Doctor of Philosophy (PhD) en https://www.repository.cam.ac.uk/handle/1810/254394 https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/334a6250-8908-4081-8b53-abe644359e7d/download 87eda9de84448d1f82354d60eee3eb5f https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c6c7f9a4-60ff-433b-9153-3946168ad98e/download 66896e4c1e085112293357dc7953dfbf https://www.rioxx.net/licenses/all-rights-reserved/