fact: Definition functorial_composition_of `{Funext} : (functorial_morphism_of TA' TB' o functorial_morphism_of TA TB)%functor = functorial_morphism_of TA'' TB''.
imports: Functor.Core NaturalTransformation.Core Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws Functor.Paths Category.Strict HoTT.Tactics PathGroupoids Types.Forall