On the syntax and the semantics of propositional dependent type theories

This thesis aims to contribute to the theory of propositional dependent type theories, also known in the literature as weak, objective, and axiomatic dependent type theories, via syntactic and semantic, specifically category theoretic, approaches. Propositional theories of dependent types are dependent type theories in which the computation rules consist of propositional equalities, rather than the definitional equalities that normally characterise the reductions and the expansions in formal systems like Martin-Löf type theory or the calculus of constructions.
Our first contribution is an analysis of the syntax of theories with identity types, dependent sum types, and dependent product types, in propositional form. Specifically, we show that dependent sum types with the reduction rule in propositional form admit, in the presence of identity types with the reduction rule in propositional form, a negative presentation. This generalises a meta-property that holds in the presence of extensional identity types. In other words, we prove how the elimination rule for dependent sum types and the corresponding reduction in propositional form are equivalent to the condition that the corresponding introduction rule enjoys the existence property in propositional form.
Secondly, we examine to what extent the deductive power of propositional theories of dependent types decreases compared to their extensional counterparts. Following an approach devised by Martin Hofmann, we prove a conservativity result for extensional theories over propositional ones, relative to the class of h-elementary statements of the latter theories i.e. the statements that are inductively obtained by quantifying over atomic h-sets. The argument exploits the soundness of the semantics of the extensional dependent type theories, which we phrase using the notion of a category with attributes as notion of a model. Informally, we show that, for judgements essentially concerning h-sets, reasoning with extensional or propositional theories is equivalent.
Finally, we focus on the semantics of propositional dependent type theories from a higher categorical perspective. Given the challenge of encoding intensional dependent type theories into 1-dimensional categorical terms and universal properties, a challenge that persists even for propositional theories, we adopt Richard Garner's approach in the 2-dimensional study of dependent types. We prove that the type constructors of propositional theories can be encoded into natural 2-dimensional category theoretic data, and we use this fact to show that the semantics of propositional theories of dependent types admits a presentation via 2-categorical models called display map 2-categories. This formulation of the semantics of propositional theories generalises the one provided by Garner for intensional ones. Our main result states that the interpretation of propositional theories within display map 2-categories is well-defined and enjoys the soundness property.