Show simple item record

dc.contributor.authorMoss, Sean
dc.date.accessioned2018-09-24T09:00:21Z
dc.date.available2018-09-24T09:00:21Z
dc.date.issued2018-10-20
dc.date.submitted2017-09-28
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/280672
dc.description.abstractThis thesis studies some constructions for building new models of Martin-Löf type theory out of old. We refer to the main techniques as gluing and idempotent splitting. For each we give general conditions under which type constructors exist in the resulting model. These techniques are used to construct some examples of Dialectica models of type theory. The name is chosen by analogy with de Paiva's Dialectica categories, which semantically embody Gödel's Dialectica functional interpretation and its variants. This continues a programme initiated by von Glehn with the construction of the polynomial model of type theory. We complete the analogy between this model and Gödel's original Dialectica by using our techniques to construct a two-level version of this model, equipping the original objects with an extra layer of predicates. In order to do this we have to carefully build up the theory of finite sum types in a display map category. We construct two other notable models. The first is a model analogous to the Diller-Nahm variant, which requires a detailed study of biproducts in categories of algebras. To make clear the generalization from the categories studied by de Paiva, we illustrate the construction of the Diller-Nahm category in terms of gluing an indexed system of types together with a system of predicates. Following this we develop the general techniques needed for the type-theoretic case. The second notable model is analogous to the Dialectica category associated to the error monad as studied by Biering. This model has only weak dependent products. In order to get a model with full dependent products we use the idempotent splitting construction, which generalizes the Karoubi envelope of a category. Making sense of the Karoubi envelope in the type-theoretic case requires us to face up to issues of coherence in our models. We choose the route of making sure all of the constructions we use preserve strict coherence, rather than applying a general coherence theorem to produce a strict model afterwards. Our chosen method preserves more detailed information in the final model.
dc.description.sponsorshipEPSRC studentship
dc.language.isoen
dc.rightsAll rights reserved
dc.rightsAll Rights Reserveden
dc.rights.urihttps://www.rioxx.net/licenses/all-rights-reserved/en
dc.subjectdependent type theory
dc.subjectcategory theory
dc.subjectcategorical logic
dc.subjectDialectica interpretation
dc.subjectfunctional interpretation
dc.titleThe Dialectica Models of Type Theory
dc.typeThesis
dc.type.qualificationlevelDoctoral
dc.type.qualificationnameDoctor of Philosophy (PhD)
dc.publisher.institutionUniversity of Cambridge
dc.publisher.departmentDepartment of Pure Mathematics and Mathematical Statistics
dc.date.updated2018-09-22T19:31:30Z
dc.identifier.doi10.17863/CAM.28036
dc.publisher.collegeTrinity College
dc.type.qualificationtitlePhD in Pure Mathematics and Mathematical Statistics
cam.supervisorHyland, Martin
cam.thesis.fundingtrue


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record