Fibred models of dual-context type theory and Kripke-Joyal forcing

Abstract

The algebraic structures that feature in constructive, presheaf-based models of homotopy type theory have been studied in two ways: using the diagrammatic reasoning of category theory, and by reasoning with judgements in the internal type theory. These approaches are connected by the standard semantics for extensional type theory in a presheaf category E, and more recently, have been explicitly related using a generalisation of Kripke-Joyal forcing semantics. An exception is the universal uniform fibration, a type-theoretic construction that requires the modal operator of crisp type theory, a fragment of Shulman's spatial type theory. Since this type theory is not internal to E, the existing methods of relating the category-theoretic and type-theoretic descriptions do not immediately apply.

Towards precisely relating these two constructions of the universal uniform fibration, we begin by identifying the categories for which crisp type theory serves as an internal language. We develop a fibred version of Awodey's natural models to capture the language's dual-context structure of modal and non-modal variables. The intended model of crisp type theory is a specific presheaf topos with an idempotent comonad; we show that any category C with an idempotent comonad admits a fibred natural model of dual-context type theory. To move to a style of semantics more convenient for later applications, we show that if C has a classifier of a stable class of maps, it admits a fibred version of a category with a classified stable class of maps that models the dual-context structure.

Next, we specialise to the intended model arising from a presheaf category E with a particular idempotent comonad. We specify how this determines a fibred category with a classified stable class of maps and show that this language validates rules of crisp type theory, notably those for crisp Pi-types. We develop Kripke-Joyal forcing semantics for this internal crisp type theory. Finally, we return to the motivating problem, using the understanding of crisp type theory as an internal language to precisely relate the category-theoretic and type-theoretic versions of the construction of a universal uniform fibration.

In addition to this main project, the thesis includes distinct work on the hyperdoctrine semantics of quantified modal logic. Lawvere hyperdoctrines give categorical semantics for intuitionistic predicate logic but are flexible enough to be applied to other logics and extended to higher-order systems. We return to Ghilardi's hyperdoctrine semantics for first-order modal logic and extend it in two directions--to weaker, non-normal modal logics and to higher-order modal logics. We also relate S4 modal hyperdoctrines to intuitionistic hyperdoctrines via a hyperdoctrinal version of the Godel-McKinsey-Tarski translation. Show more