Adjoint logic with a 2-category of modes

Abstract

We generalize the adjoint logics of Benton and Wadler [1994, 1996] and Reed [2009] to allow multiple different adjunctions between the same categories. This provides insight into the structural proof theory of cohesive homotopy type theory, which integrates the synthetic homotopy theory of homotopy type theory with the synthetic topology of Lawvere’s axiomatic cohesion. Reed’s calculus is parametrized by a preorder of modes, where each mode determines a category, and there is an adjunction between categories that are related by the preorder. Here, we consider a logic parametrized by a 2-category of modes, where each mode represents a category, each mode morphism represents an adjunction, and each mode 2-morphism represents a pair of conjugate natural transformations. Using this, we give mode theories that describe adjoint triples of the sort used in cohesive homotopy type theory. We give a sequent calculus for this logic, show that identity and cut are admissible, show that this syntax is sound and complete for pseudofunctors from the mode 2-category to the 2-category of adjunctions, and investigate some constructions in the example mode theories.