Contextads as Wreaths; Kleisli, Para, and Span Constructions as Wreath Products

TL;DR

This paper introduces contextads and the Ctx construction, unifying various category theory structures related to context and contextful arrows, with applications to functional programming and side-effects modeling.

Contribution

It defines contextads using wreaths, establishes the Ctx construction's universal property, and explores their role in organizing contextful computation and monads.

Findings

Unified framework for context and contextful arrows in category theory

Demonstrated that many side-effects monads can be captured by dependently graded comonads

Proved the trifunctoriality of the Ctx construction

Abstract

We introduce contextads and the Ctx construction, unifying various structures and constructions in category theory dealing with context and contextful arrows -- comonads and their Kleisli construction, actegories and their Para construction, adequate triples and their Span construction. Contextads are defined in terms of Lack--Street wreaths, suitably categorified for pseudomonads in a tricategory of spans in a 2-category with display maps. The associated wreath product provides the Ctx construction, and by its universal property we conclude trifunctoriality. This abstract approach lets us work up to structure, and thus swiftly prove that, under very mild assumptions, a contextad equipped colaxly with a 2-algebraic structure produces a similarly structured double category of contextful arrows. We also explore the role contextads might play qua dependently graded comonads in organizing contextful computation in functional programming. We show that many side-effects monads can be dually captured by dependently graded comonads, and gesture towards a general result on the `transposability' of parametric right adjoint monads to dependently graded comonads.