I can see three ways to "do formal category theory":


1. Yoneda structures à la Street-Walters.
2. cosmoi à la Street.
3. proarrow equipments.


It seems to me that 2. is older than 1., and a particular case thereof (you impose more requests on $y\_A : A \to PA$ asking that there is an adjoint to the pseudofunctor $P : {\cal K}^\text{coop} \to {\cal K}$).


Is there, instead, a relation between Yoneda structures, cosmoi, and proarrow equipments?



How do the existing ways to do formal CT relate to each other?
Street's "fibrational cosmoi" are indeed a special case of, or rather a particular way to construct, a Yoneda structure. They are substantially less general, since Yoneda structures and equipments include the case of enriched categories, but fibrational cosmoi do not. (Street also used the word "cosmos" later for a bicategory of the form $W \mathrm{Prof}$, which is more like the horizontal part of an equipment, but doesn't contain information about the functors as distinct from the representable profunctors.)


Yoneda structures and equipments are similar in that they both enhance a 2-category with information about "profunctors", but they do it in slightly different ways, so that in constructing examples one has to make different choices about how to deal with size. Namely, in an equipment (as originally defined), all proarrows are composable; thus if we include large categories as objects, we also need to include large-set-valued profunctors as proarrows; or we can consider only small categories and small-set-valued profunctors. On the other hand, in a Yoneda structure all profunctors are small-"set"-valued, but we are required to include large categories and even "locally large" categories, since the presheaf category of a non-small category is not generally locally small; thus not every category has an identity proarrow and not all proarrows can be composed.


Thus, although morally they contain about the same information, it's hard to prove a precise comparison abstractly. The best I'm aware of is [this paper](https://arxiv.org/abs/1511.04070) of Koudenburg, which uses a generalization of equipments to "hypervirtual double categories" and shows that under reasonable assumptions, presheaf categories can be given a universal property therein that corresponds exactly to the axioms of a Yoneda structure on a certain subcategory.


