On the unicity of formal category theories

Abstract

We prove an equivalence between cocomplete Yoneda structures and certain proarrow equipments on a 2-category $\mathcal{K}$. In order to do this, we recognize the presheaf construction of a cocomplete Yoneda structure as a relative, lax idempotent monad sending each admissible 1-cell $f:A\to B$ to an adjunction ${\mathbf{P}}_{!}f⊣{\mathbf{P}}^{\ast }f$. Each cocomplete Yoneda structure on $\mathcal{K}$ arises in this way from a relative lax idempotent monad "with enough adjoint 1-cells", whose domain generates the ideal of admissibles, and the Kleisli category of such a monad equips its domain with proarrows. We call these structures "yosegi". Quite often, the presheaf construction associated to a yosegi generates an ambidextrous Yoneda structure; in such a setting there exists a fully formal version of Isbell duality.

38 pages