Semantics of multimodal adjoint type theory

TL;DR

This paper introduces Multimodal Adjoint Type Theory (MATT), a new framework that interprets complex multimodal type theories within diagrams of categories, utilizing a construction called co-dextrification to handle adjoints.

Contribution

It provides a novel interpretation method for multimodal type theories in arbitrary diagrams of categories without requiring extra left adjoints, and introduces MATT as a unified modal type theory.

Findings

Interpretation of MTT in any M-shaped diagram of categories

Introduction of co-dextrification to add left adjoints

Interpretation of MATT in diagrams of toposes and geometric morphisms

Abstract

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.