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