Adjoint Logic with a 2-Category of Modes

We generalize the adjoint logics of Benton and Wadler (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 morphism of adjunctions. For example, using this, we can give a mode theory for an adjoint triple L M R by using two mode morphisms to generate two adjunctions between the same two categories, and then using mode 2-cells to identify the right adjoint of one with the ...

• Type: Journal
• Year: 2016
• Where: LFCS
• Authors: Daniel R. Licata, Michael Shulman
• Keywords: Artificial Intelligence, LFCS 2016