{ T : NaturalTransformation 1 (G o F) | forall (c : C) (d : D) (f : morphism C c (G d)), Contr { g : morphism D (F c) d | G _1 g o T c = f } }.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Dual Functor.Dual NaturalTransformation.Dual. Require Import Functor.Composition.Core Functor.Identity.