Higher-dimensional realizability for intensional type theory
<p>We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry higher-dimensional structure. In the spirit of realizability this is intended to formalise a higher-dimensional (topological, homotopical) BHK interpretation whereby evidence f...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2023
|
| Subjects: |
| _version_ | 1826313371995078656 |
|---|---|
| author | Speight, SL |
| author2 | Abramsky, S |
| author_facet | Abramsky, S Speight, SL |
| author_sort | Speight, SL |
| collection | OXFORD |
| description | <p>We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry higher-dimensional structure. In the spirit of realizability this is intended to formalise a higher-dimensional (topological, homotopical) BHK interpretation whereby evidence for an identification is a path.</p>
<br>
<p>The parameter over which we build realizability models is a "realizer category". These are equipped with an interval <em>qua</em> internal co-groupoid, which facilitates a notion of homotopy in the ambient category, as well as a fundamental groupoid construction on it. In groupoidal realizability, objects of a base groupoid are realized by points in the fundamental groupoid of some object from the realizer category, and the isomorphisms from the base groupoid are realized by paths in that fundamental groupoid.</p>
<br>
<p>We first explain why a naive formulation of groupoidal assemblies is not fit for modelling type theory; this motivates studying <em>partitioned</em> groupoidal assemblies.</p>
<br>
</p>The main result of the thesis is that, when the realizer category is finitely complete in a suitable sense, the ensuing category of partitioned groupoidal assemblies is a path category with weak dependent products, hence a model of a version of intensional (1-truncated) type theory with dependent products and without function extensionality. When the underlying realizer category is "untyped", there exists an impredicative universe of 1-types, given by the modest fibrations.</p> |
| first_indexed | 2024-09-25T04:12:05Z |
| format | Thesis |
| id | oxford-uuid:5afb6d38-08df-4df6-8b09-dd85e7766860 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:12:05Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | oxford-uuid:5afb6d38-08df-4df6-8b09-dd85e77668602024-07-04T11:24:36ZHigher-dimensional realizability for intensional type theoryThesishttp://purl.org/coar/resource_type/c_db06uuid:5afb6d38-08df-4df6-8b09-dd85e7766860Categories (mathematics)Symbolic and mathematical logicCurry-Howard isomorphismEnglishHyrax Deposit2023Speight, SLAbramsky, SStaton, S<p>We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry higher-dimensional structure. In the spirit of realizability this is intended to formalise a higher-dimensional (topological, homotopical) BHK interpretation whereby evidence for an identification is a path.</p> <br> <p>The parameter over which we build realizability models is a "realizer category". These are equipped with an interval <em>qua</em> internal co-groupoid, which facilitates a notion of homotopy in the ambient category, as well as a fundamental groupoid construction on it. In groupoidal realizability, objects of a base groupoid are realized by points in the fundamental groupoid of some object from the realizer category, and the isomorphisms from the base groupoid are realized by paths in that fundamental groupoid.</p> <br> <p>We first explain why a naive formulation of groupoidal assemblies is not fit for modelling type theory; this motivates studying <em>partitioned</em> groupoidal assemblies.</p> <br> </p>The main result of the thesis is that, when the realizer category is finitely complete in a suitable sense, the ensuing category of partitioned groupoidal assemblies is a path category with weak dependent products, hence a model of a version of intensional (1-truncated) type theory with dependent products and without function extensionality. When the underlying realizer category is "untyped", there exists an impredicative universe of 1-types, given by the modest fibrations.</p> |
| spellingShingle | Categories (mathematics) Symbolic and mathematical logic Curry-Howard isomorphism Speight, SL Higher-dimensional realizability for intensional type theory |
| title | Higher-dimensional realizability for intensional type theory |
| title_full | Higher-dimensional realizability for intensional type theory |
| title_fullStr | Higher-dimensional realizability for intensional type theory |
| title_full_unstemmed | Higher-dimensional realizability for intensional type theory |
| title_short | Higher-dimensional realizability for intensional type theory |
| title_sort | higher dimensional realizability for intensional type theory |
| topic | Categories (mathematics) Symbolic and mathematical logic Curry-Howard isomorphism |
| work_keys_str_mv | AT speightsl higherdimensionalrealizabilityforintensionaltypetheory |