White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Models of Dependent Type Theory from Algebraic Weak Factorisation Systems

Larrea, Marco Federico (2018) Models of Dependent Type Theory from Algebraic Weak Factorisation Systems. PhD thesis, University of Leeds.

Text (PhD thesis )
HardBindVersion2-Thesis-MarcoLarrea.pdf - Final eThesis - complete (pdf)
Available under License Creative Commons Attribution-Noncommercial-Share Alike 2.0 UK: England & Wales.

Download (1048Kb) | Preview


The main purpose of this dissertation is to analyse the extent to which algebraic weak factorisation systems provide models of Martin-L ̈of dependent type theory. To this end, we develop the notion of a type-theoretic awfs; this is a category equipped with an algebraic weak factorisation system and some additional structure, such that after performing a splitting procedure, a model of Martin-L ̈of dependent type theory is obtained. We proceed to construct examples of such type-theoretic awfs’s; first in the category of small groupoids, which produces the Hofmann and Streicher groupoid model. Later we make use of the machinery of uniform fibrations of Gambino and Sattler to produce type-theoretic awfs’s in Grothendieck toposes equipped with an interval object satisfying some additional properties; from this we obtain concrete examples in the categories of simplicial sets and cubical sets. We also study the notion of a normal uniform fibration, a strengthening of the notion of a uniform fibration, which allows us to address a question regarding the constructive nature of type-theoretic awfs’s. In addition, we show that the procedure of constructing type-theoretic awfs’s from uniform fibrations is functorial, thus providing a method for comparing models of dependent type theory.

Item Type: Thesis (PhD)
Keywords: Mathematics, Logic, Algebraic Topology, Type Theory, Category Theory, HoTT
Academic Units: The University of Leeds > Faculty of Maths and Physical Sciences (Leeds) > School of Mathematics (Leeds) > Pure Mathematics (Leeds)
Identification Number/EthosID: uk.bl.ethos.770050
Depositing User: Marco Federico Larrea
Date Deposited: 01 Apr 2019 09:38
Last Modified: 18 Feb 2020 12:49
URI: http://etheses.whiterose.ac.uk/id/eprint/23032

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)