Bimodule

A bimodule from $\mathcal{O}:\mathcal{C}\to \mathcal{D}$ provides for all $x:\mathcal{C};y:\mathcal{D}$ a homset $\mathcal{O}(x,y)$ and compose these $\mathcal{O}$-morphisms. This is subject to 5 laws.

See also

Profunctor