fact: Definition inverse_object_of_morphism_of s d (m : morphism C1 s d) : morphism (C2 -> D) (inverse_object_of_object_of s) (inverse_object_of_object_of d).
imports: Category.Core Category.Prod FunctorCategory.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths Basics.Tactics