Relative pseudo-monads

Nicola Gambino, University of Leeds. Part of the proofs, constructions and computations seminar series.

Working in the IZF, the assignment mapping a set X to the class of its subsets Pow(X) can easily be shown to be part of a monad thanks to the power set axiom. But working in CZF, which does not have the power-set axiom, this assignment is only part of a "relative monad”, a notion defined by Altenkirch, Chapman and Uustalu. A similar situation arises in category theory: the assignment mapping a small category C to its category of presheaves Psh(C) is not a monad. This time this is both because of size reasons (even working in IZF) and coherence reasons (the axioms for a relative monad do not hold strictly). In this talk, I will introduce the notion of a relative pseudo-monad, which axiomatizes the essential properties of the presheaf construction, and illustrate some of its applications, including a conceptual reconstruction of a 2-categorical model of linear logic and the differential lambda-calculus. This is joint work with Marcelo Fiore, Martin Hyland, and Glynn Winskel (arXiv:1612.03678).

Nicola Gambino, University of Leeds