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

Polynomial functors and W-types for groupoids

Vidmar, Jakob (2018) Polynomial functors and W-types for groupoids. PhD thesis, University of Leeds.

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

Download (759Kb) | Preview


This thesis contributes to the semantics of Martin-Lof type theory and the theory of polynomial functors. We do so by investigating polynomial functors on the category of groupoids and their initial algebras, known as W-types. We consider several versions of polynomial functors: both simple and dependent, associated to either split, cloven or general fibrations. Our main results show the existence of W-types and their pullback stability in a variety of situations. These results are obtained working constructively, ie avoiding the use of excluded middle, the axiom of choice, power set axiom, ordinal iteration. We also extend the theory of natural models, by defining a version of them for Martin-Lof type theories where eta-equality holds up to propositional, and not definitional equality.

Item Type: Thesis (PhD)
Keywords: Category Theory, Type Theory, Groupoids, Polynomial Functors, W-Types
Academic Units: The University of Leeds > Faculty of Maths and Physical Sciences (Leeds) > School of Mathematics (Leeds) > Pure Mathematics (Leeds)
Depositing User: Mr Jakob Vidmar
Date Deposited: 21 Feb 2019 13:45
Last Modified: 21 Feb 2019 13:45
URI: http://etheses.whiterose.ac.uk/id/eprint/22517

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)