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

Homotopy Type-Theoretic Interpretations of Constructive Set Theories

Gallozzi, Cesare (2018) Homotopy Type-Theoretic Interpretations of Constructive Set Theories. PhD thesis, University of Leeds.

Gallozzi_C_Mathematics_PhD_2018.pdf - Final eThesis - complete (pdf)
Available under License Creative Commons Attribution-Noncommercial-Share Alike 2.0 UK: England & Wales.

Download (831Kb) | Preview


This thesis deals primarily with type-theoretic interpretations of constructive set theories using notions and ideas from homotopy type theory. We introduce a family of interpretations [.]_k,h for 2 ≤ k ≤ ∞ and 1 ≤ h ≤ ∞ of the set theory BCS into the type theory H, in which sets and formulas are interpreted respectively as types of homotopy level k and h. Depending on the values of the parameters k and h we are able to interpret different theories, like Aczel's CZF and Myhill's CST. We relate the family [.]_k,h to the other interpretations of CST into homotopy type theory already studied in the literature in [UFP13] and [Gy16a]. We characterise a class of sentences valid in the interpretations [.]_k,∞ in terms of the ΠΣ axiom of choice, generalising the characterisation of [RT06] for Aczel's interpretation. We also define a proposition-as-hproposition interpretation in the context of logic-enriched type theories. The formulas valid in this interpretation are then characterised in terms of the axiom of unique choice. We extend the analysis of Aczel's interpretation provided in [GA06] to the interpretations of CST into homotopy type theory, providing a comparative analysis. This is done formulating in the logic-enriched type theory the key principles used in the proofs of the two interpretations. We also investigate the notion of feasible ordinal formalised in the context of a linear type theory equipped with a type of resources. This type theory was originally introduced by Hofmann in [Hof03]. We disprove Hofmann's conjecture on the definable ordinals, by showing that for any given k ϵ N the ordinal ω^k is definable.

Item Type: Thesis (PhD)
Keywords: Homotopy Type Theory, Constructive Set Theory, Linear Type Theory
Academic Units: The University of Leeds > Faculty of Maths and Physical Sciences (Leeds) > School of Mathematics (Leeds) > Pure Mathematics (Leeds)
Depositing User: Cesare Gallozzi
Date Deposited: 11 Dec 2018 11:18
Last Modified: 11 Dec 2018 11:18
URI: http://etheses.whiterose.ac.uk/id/eprint/22317

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)