作为花环的上下文单子；Kleisli、Para 和 Span 构造作为花环积

我们引入了上下文单子 (contextads) 和 Ctx 构造，统一了范畴论中处理上下文和上下文相关箭头的各种结构和构造——余单子及其 Kleisli 构造、作用范畴及其 Para 构造、恰当三元组及其 Span 构造。上下文单子是根据 Lack-Street 花环 (wreaths) 定义的，并针对具有展示映射的 2-范畴中的 span 三范畴中的伪单子进行了适当的范畴化。相关联的花环积提供了 Ctx 构造，并且通过其泛性质，我们得出了三函子性。这种抽象方法使我们能够处理结构本身，从而迅速证明，在非常温和的假设下，一个 lax 余配以 2-代数结构的上下文单子会产生一个具有类似结构的上下文元素双范畴。我们还探讨了上下文单子作为依赖类型分次余单子在组织函数式编程中的上下文相关计算方面可能扮演的角色。我们展示了许多副作用单子可以被依赖类型分次余单子对偶地捕获，并暗示了关于参数右伴随单子到依赖类型分次余单子的“可转置性”的一般结果。