fact: Definition pretensor (A : C) := Core.induced_snd tensor A.
imports: Basics.Utf8 Category.Core Category.Morphisms Functor.Core Functor.Utf8 NaturalTransformation.Core FunctorCategory.Core FunctorCategory.Morphisms ProductLaws