fact: Definition opposite C D (F G : Functor C D) (T : NaturalTransformation F G) : NaturalTransformation G^op F^op := Build_NaturalTransformation' (G^op) (F^op) (components_of T) (fun s d => commutes_sym T d s) (fun s d => commutes T d s).
imports: Category.Core Functor.Core NaturalTransformation.Core