(Note that we write compositions from left to right and accordingly apply most maps on the right.)

**Def.1**

A functor is called a *left adjoint* to a functor if there is a bijection between the homsets:

natural in both and . In this case is called a right adjoint to , and we write .

**Def.2**

A functor is called a *left adjoint* to a functor if there are natural transformations and satisfying the *zig-zag identities*:

So, *why* are these two definitions equivalent?

We start out from Def.2, as it generalizes to arbitrary bicategory or double category, which enable morphisms (‘*transformations*‘ or ‘*2-cells*‘) between [parallel] arrows. Transformations will be depicted by a dashed arrow symbol: .

We are using the bicategory which has functors as arrows and natural transformations as transformations, and the bicategory which has profunctors as arrows. And we are going to pass them both to Ehresmann’s double category construction of ‘*quintets*‘.

In short, we will obtain a full inclusion of (doubly weak) double categories of the quintets of into that of which is covariant for vertical arrows but contravariant for horizontal arrows, hence taking adjunctions to companions and companions to adjunctions.

Noting that companions are just ismorphisms in the ambient bicategory, we will conclude that an adjunction in corresponds to an isomorphism in and a natural isomomorphism (in particular, the identity of any functor) in corresponds to an adjunction in .

Note that, both sides of the natural bijection in Def.1 are functors , i.e. are *profunctors*.

Specifically, they above are denoted by and , that is, for a single functor , we define

In the terminology of heteromorphisms, we can get if we take a copy from each arrow in of the form and regard them as heteromorphisms . The copy of is a *reflection arrow* (into the full subcategory ), these generate the profunctor .

Similarly, is generated by the *coreflection arrows* .

Importantly, it turns out that there is an adjunction in the bicategory of categories and profunctors, for any functor (according to Def.2).

In the setting of bicategories [double categories], one can already prove uniqueness of left/right adjoint for a given arrow (up to isomorphism) and the following interchanging rules, which assert one-to-one correspondences between the transformations below, supposed :

The mappings and extend to two natural embeddings of the bicategory , whose arrows are the functors, into .

Note that is contravariant on arrows (reverses source/target and composition of functors) while is contravariant on the natural transformations.

To express these as covariant mappings, the notations and are introduced for the bicategory obtained from by reversing arrows / transformations, respectively.

Using the interchange rules, we show below how to arrive to the embedding when starting out from , touching an embedding of *double categories*, , in the middle of the way:

A diagram of functors with induces and is determined by any of the following profunctor morphisms:

In a *double category*, transformations are supported by a pair of ‘*vertical arrows*‘ (regarding the original arrows as horizontal ones), and thus are depicted and also called as *squares* (or ‘cells’).

Horizontally adjacent squares, as well as horizontal arrows can be associatively composed horizontally, with units.

Vertically adjacent squares, as well as vertical arrows can be associatively composed vertically, with units.

The so called *Ehresmann* double category can be defined for any bicategory : all the arrows of are considered both vertical and horizontal in , with squares as transformations .

Now we are ready to define our embedding : its source is the double category , and its target is the double category , and flips horizontal arrows and horizontal composition.

So that . All objects (the categories) are fixed, a horizontal arrow (a functor ) is mapped to , while a vertical arrow (a functor ) is mapped to and a square is mapped to the corresponding square of . Compositions just work fine.

Explicitly, sends the pair of generating heteromorphisms to the composite for any .

Adjunction in a double category is interpreted between a *vertical* and *horizontal* , in such a way that in for a bicategory translates readily to being left adjoint to in , according to Def.2.

If we flip horizontal arrows in a double category, adjunctions become *companions*:

A pair of horizontal and vertical arrows , are said to be a *companion* pair, if there exist squares as below

such that and (vertical composition) .

It is easy to see, that a companion in is just a pair of parallel isomorphic arrows in .

Since flips horizontal arrows, takes adjunctions to companions and companions to adjunctions.

Moreover, is surjective on squares.

Put it all together, we get that

two functors are naturally isomorphic if and only if there is an adjunction of profunctors . (This is basically one of the key observations above that .)

And, finally,

two functors are adjoint according to Def.2 if and only if we have an isomorphism of profunctors , i.e. Def.1 holds.

**Remark.** Actually, there are issues about formalizing Ehresmann’s construction for general bicategories.

When composition of arrows in a bicategory is strictly associative, we indeed get a (still strictly associative) double category . Otherwise, however, the resulting double category would be only *weakly* associative both horizontally and vertically, and such animals can only be defined by workarounds, e.g. using higher dimension categories with special collapses.

But don’t panic, we can still make things precise by introducing adequate maps from double categories to bicategories, so that would become such a map , with all its good properties, in particular taking companions to adjunctions and an adjunction to a pair of isomorphic arrows.