On the unicity of formal category theories

TL;DR

This paper establishes an equivalence between cocomplete Yoneda structures and proarrow equipments on a 2-category, introducing the concept of 'yosegi' structures and exploring their relation to presheaf constructions and Isbell duality.

Contribution

It introduces 'yosegi' structures as a new framework linking cocomplete Yoneda structures with proarrow equipments via relative lax idempotent monads.

Findings

Equivalence between cocomplete Yoneda structures and proarrow equipments.

Introduction of 'yosegi' structures as a new conceptual framework.

Formalization of Isbell duality in the context of presheaf constructions.

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 $\boldsymbol{P}_!f\dashv\boldsymbol{P}^*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.