fact: Definition functor_composition_of s d d' (m1 : morphism ((C -> D) * (C -> D')) s d) (m2 : morphism ((C -> D) * (C -> D')) d d') : functor_morphism_of (m2 o m1) = functor_morphism_of m2 o functor_morphism_of m1.
imports: Category.Core Functor.Core Functor.Prod.Core FunctorCategory.Core Category.Prod NaturalTransformation.Prod NaturalTransformation.Composition.Core NaturalTransformation.Paths