Higher-dimensional realizability for intensional type theory

Thesis

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.

The parameter over which we build realizability models is a "realizer category". These are equipped with an interval qua 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.

We first explain why a naive formulation of groupoidal assemblies is not fit for modelling type theory; this motivates studying partitioned groupoidal assemblies.

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.

Authors: Speight, SL

• DOI: 10.5287/ora-9onp0gxry
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: realizability; type theory; groupoids
• Subjects: Categories (mathematics); Symbolic and mathematical logic; Curry-Howard isomorphism