Abstracts.2018.InternalizingVariance

Internalizing variance using 2-categories

by Sandro Stucki

The notion of "variance", "monotonicity" or "polarity" of operations is ubiquitous in the meta-theory of logics and programming languages, but it is seldom reflected into the syntax of such languages, so that a programmer or logician can reason directly about monotone functions. In this talk I will present a modal extension to the simply-typed lambda calculus that allows reasoning about ordered terms and monotone functions defined over them. I will show that the usual categorical semantics of STLC as CCCs can be extended to a 2-categorical semantics that covers the extra order-theoretic structure. Since I don't expect any prior knowledge about higher category theory, I will also give a brief intro to 2-categories.