Orthogonality Axioms in Type Theory

Specialeforsvar ved Magnus Baunsgaard Kristensen

Titel: Orthogonality Axioms in Type Theory

Abstract: In this thesis we give a presentation of dependent type theory, and discuss how to model it in presheaf categories. The discussion is centered around the intensional Martin-Löf type theory, touching on both the classic connection to proof theory and the more recent advances in relating such theories to homotopy theory known as homotopy type theory. The presheaf semantics are based on (M. Hoffman, 1997), in which the model is presented in the more general setting of categories with families; the primary focus here is hence giving presheaf categories the structure of a category with families. We extend this theory, and consequently the model of this theory, in three ways through out the thesis. First we will discuss how to add a fix point combinator to dependent type theory without introducing inconsistencies into the theory, and how to encode the coinductive type of streams in this theory. This idea is based on guarded recursion as proposed in (H. Nakano, 2000), and a variant of if it is put into programmatic practice in (R. Atkey and C. McBride, 2013). We provide a model for this theory with a clock irrelevance axiom in a certain presheaf category and show that clock irrelevance can be modelled as orthogonality to an object of clocks, following (A. Bizjak and R. Møgelberg, 2018). We then consider an implementation of an intensional identity type in cubical type theory. The presentation of cubical type theory follows (C. Cohen et al., 2016), and in particular we implement path types as a function space from an abstract interval; the interval is here assumed to have the structure of a de Morgan algebra. Path types are given the structure of an intensional identity type using composition operations on types. The theory is modelled in the category of cubical sets, based on a presentation of cubical sets compatible with the de Morgan structure on the syntactic interval. Cubical sets support a notion of Kan fibrations, a notion known from the setting of simplicial sets, which we modify and relate to the composition structure in the theory. Finally, we show that guarded dependent type theory is consistent with the addition of intensional identity types implemented as path types. We do this by presenting a hybrid of the two other theories, rephrasing the clock irrelevance axiom presented in (A. Bizjak and R. Møgelberg, 2018) as a path equality of terms. We model this theory in a certain presheaf category based on the previously presented models. In particular, the modified clock irrelevance axiom is modelled using an orthogonality condition.

Vejleder:  Jesper Michael Møller
Censor:    Lisbeth Fajstrup, AAU