fact: Definition slice_category_induced_functor F' a' (m : morphism D a a') (T : NaturalTransformation F' F) : Functor (F / a) (F' / a') := comma_category_induced_functor (s := (F, !a)) (d := (F', !a')) (T, @slice_category_induced_functor_nt 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