fact: Definition cat_over_induced_functor a a' (m : morphism cat a a') : Functor (cat / a) (cat / a') := slice_category_over_induced_functor cat a a' m.
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Dual Category.Prod NaturalTransformation.Identity FunctorCategory.Core Cat.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors HoTT.Tactics Basics.Tactics