F' a' (m : morphism D a' a) (T : NaturalTransformation F F') : Functor (a / F) (a' / F') := comma_category_induced_functor (s := (!a, F)) (d := (!a', F')) (@slice_category_induced_functor_nt a' a m, T).
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Dual. Require Import Category.Prod. Require Import NaturalTransformation.Identity. Require Import FunctorCategory.Core Cat.Core. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors. Import Comma.Core. Require Import HoTT.Tactics. Require Import Basics.Tactics.