fact: Variable H : Functor A B.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Functorial.Core NaturalTransformation.Composition.Core NaturalTransformation.Isomorphisms Functor.Attributes FunctorCategory.Core Category.Morphisms NaturalTransformation.Paths HoTT.Truncations.Core