Sciweavers

Share
LFCS
2016
Springer

Adjoint Logic with a 2-Category of Modes

4 years 3 months ago
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 ...
Daniel R. Licata, Michael Shulman
Added 07 Apr 2016
Updated 07 Apr 2016
Type Journal
Year 2016
Where LFCS
Authors Daniel R. Licata, Michael Shulman
Comments (0)
books