We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-sized limits, without the need for extra left adjoints. This is achieved by a construction called “co-dextrification” that co-freely adds left adjoints to any such diagram, which can then be used to interpret the “context lock” functors of MTT. Furthermore, if any of the functors in the diagram have right adjoints, these can also be internalized in type theory as negative modalities in the style of FitchTT. We introduce the name Multimodal Adjoint Type Theory (MATT) for the resulting combined general modal type theory. In particular, we can interpret MATT in any finite diagram of toposes and geometric morphisms, with positive modalities for inverse image functors and negative modalities for direct image functors.

Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. Here we focus on MTT [Daniel Gratzer et al., 2021], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [Birkedal et al., 2020]. These modalities are specified by mode theories [Licata and Shulman, 2016], 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities. We contribute a defunctionalized NbE algorithm which reduces the type-checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories - mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type-checking algorithm. We further contribute mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.

We prove the conjecture that any Grothendieck $(\infty ,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to $(\infty ,1)$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.

We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental ∞-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer’s fixed-point theorem.