Show simple item record

dc.contributor.authorOrton, Richard Ian
dc.description.abstractThis thesis presents an account of the cubical sets model of homotopy type theory using an internal type theory for elementary topoi. Homotopy type theory is a variant of Martin-Lof type theory where we think of types as spaces, with terms as points in the space and elements of the identity type as paths. We actualise this intuition by extending type theory with Voevodsky's univalence axiom which identifies equalities between types with homotopy equivalences between spaces. Voevodsky showed the univalence axiom to be consistent by giving a model of homotopy type theory in the category of Kan simplicial sets in a paper with Kapulkin and Lumsdaine. However, this construction makes fundamental use of classical logic in order to show certain results. Therefore this model cannot be used to explain the computational content of the univalence axiom, such as how to compute terms involving univalence. This problem was resolved by Cohen, Coquand, Huber and Mortberg, who presented a new model of type theory in Kan cubical sets which validated the univalence axiom using a constructive metatheory. This meant that the model provided an understanding of the computational content of univalence. In fact, the authors present a new type theory, cubical type theory, where univalence is provable using a new "glueing" type former. This type former comes with appropriate definitional equalities which explain how the univalence axiom should compute. In particular, Huber proved that any term of natural number type constructed in this new type theory must reduce to a numeral. This thesis explores models of type theory based on the cubical sets model of Cohen et al. It gives an account of this model using the internal language of toposes, where we present a series of axioms which are sufficient to construct a model of cubical type theory, and hence a model of homotopy type theory. This approach therefore generalises the original model and gives a new and useful method for analysing models of type theory. We also discuss an alternative derivation of the univalence axiom and show how this leads to a potentially simpler proof of univalence in any model satisfying the axioms mentioned above, such as cubical sets. Finally, we discuss some shortcomings of the internal language approach with respect to constructing univalent universes. We overcome these difficulties by extending the internal language with an appropriate modality in order to manipulate global elements of an object.
dc.description.sponsorshipUK EPSRC PhD studentship, funded by grants EP/L504920/1, EP/M506485/1.
dc.rightsAttribution 4.0 International (CC BY 4.0)
dc.subjecttype theory
dc.subjecthomtopy type theory
dc.subjectunivalent type theory
dc.subjectcubical type theory
dc.subjectcubical sets
dc.subjectinternal language
dc.titleCubical Models of Homotopy Type Theory - An Internal Approach
dc.type.qualificationnameDoctor of Philosophy (PhD)
dc.publisher.institutionUniversity of Cambridge
dc.publisher.departmentComputer Science and Technology
dc.contributor.orcidOrton, Richard Ian [0000-0002-9924-0623]
dc.type.qualificationtitlePhd in Computer Science
cam.supervisorPitts, Andrew Mawdesley
cam.supervisor.orcidPitts, Andrew Mawdesley [0000-0001-7775-3471]

Files in this item


This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International (CC BY 4.0)
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)