Uemura develops a general framework for relating the syntax of type theory and semantics of dependent type theory of dependent type theories. He defines an abstract type theory as a category with representable maps, with models given by suitable structure-preserving functors into categories of discrete fibrations. To connect this semantic account with conventional presentations by judgments and inference rules, he introduces second-order generalized algebraic theories (SOGATs), showing that they generate abstract type theories and that every abstract type theory admits such a presentation. This yields a general theory-model correspondence, providing a categorical justification for treating models as having internal languages. The thesis also extends this account to -type theories1, using them to formulate coherence problems for non-split and higher-categorical models and to sketch an internal-language result for finitely complete -categories.
The latter part of the thesis applies this framework to HoTT. Uemura reformulates cubical model constructions within the preceding notion of model and studies the resulting cubical assembly model. This model provides consistency and independence results concerning univalence, impredicative universes, Propositional Resizing, Markov’s principle, and Church’s thesis: in particular, it supports a univalent impredicative universe while refuting propositional resizing, and a reflective subuniverse is constructed in which both Markov’s Principle and Church’s Thesis hold. Thus the thesis combines a general categorical account of type theories with a concrete semantic investigation of principles compatible with univalent foundations.