Here we use the context of Definition 1. (or, equivalently, of Definition 2.) of page ‘Many Faces of a Profunctor’, that is, we identify a profunctor (according to Definition 3.) with the category that disjointly contains (isomorphic copies of) and and for all objects , the set is considered as the homset and its elements are called heteromorphisms. Their compositions with arrows of (from the left) and arrows of (from the right) are given by the action of the functor on the arrows.
This setup naturally induces a functor where is the category of two objects and a single nonidentity arrow whose preimage at is exactly the collection of all heteromorphisms in .
In this setting we write to express that is a profunctor from category to category .
Definition. Let and be profunctors . By a profunctor morphism we simply mean a functor such that both of its restrictions, to and to , are the identity functors.
Note that such a functor indeed straightly corresponds to a natural transformation where are .
Definition. A given profunctor is said to be generated by a class of heteromorphisms if every heteromorphism can be written in the form for some .
Definition. Let and be profunctors. Their profunctor composition is the profunctor whose heteromorphisms are formal compositions (i.e. ordered pairs) of consecutive heteromorphisms and , subject to the (tensor-like) relation that is considered equal to for any configuration .
This is basically the free composition of and , and we can actually relax it in the spirit of Definition 2.
For that, let denote the preorder category of the three element ordered set , i.e. it has three objects: and three nonidentity arrows: and their composition .
Definition. Let and be profunctors with and . We call a category equipped with a functor , a (realized) ternary composition of and , if the preimage of at is and the preimage of at is .
(Naturally, this condition can be easily rephrased using pullbacks for expressing the preimages.)
Theorem. For fixed profunctors and , there is a correspondence between their ternary compositions and profunctor morphisms of the form where is any profunctor .
Proof. For a given ternary composition we can define by simply deleting () from and map the formal composition of consecutive heteromorphisms to their actual composition defined in .
For a given profunctor morphism we can define the category as basically the union of and such that the composition of consecutive heteromorphisms is defined to be .
Corollary. We could have defined the composition of profunctors as the initial object in the category of their ternary compositions.