C D (F G : Functor C D) (T : NaturalTransformation F G) : (T^op)^op = T := idpath.
Import Category.Dual.CategoryDualNotations Functor.Dual.FunctorDualNotations. Require Import Category.Core Functor.Core NaturalTransformation.Core.