fact: Definition functor_identity_of (x : object ((C -> D) * (C -> D'))) : functor_morphism_of (identity x) = identity _.
imports: Category.Core Functor.Core Functor.Prod.Core FunctorCategory.Core Category.Prod NaturalTransformation.Prod NaturalTransformation.Composition.Core NaturalTransformation.Paths