C D (F : Functor C D) : D -|-> C := 1%profunctor o (F^op, 1).
Require Import Category.Core Functor.Core Functor.Prod.Core Profunctor.Core Functor.Dual Profunctor.Identity Functor.Composition.Core Functor.Identity.