fact: Record NaturalTransformation := Build_NaturalTransformation' { components_of :> forall c, morphism D (F c) (G c); commutes : forall s d (m : morphism C s d), components_of d o F _1 m = G _1 m o components_of s; commutes_sym : forall s d (m : C.(morphism) s d), G _1 m o components_of s = components_of d o F _1 m }.
imports: Category.Core Functor.Core