Functor (S / T) (S' / T'). Proof. refine (Build_Functor (S / T) (S' / T') functorial_morphism_of_object_of functorial_morphism_of_morphism_of _ _); abstract ( intros; apply CommaCategory.path_morphism; simpl; auto with functor ). Defined.
Require Import Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core. Require Import NaturalTransformation.Composition.Laws. Require Import Functor.Paths. Require Import Category.Strict. Import Comma.Core. Import Functor.Identity.FunctorIdentityNotations NaturalTransformation.Identity.NaturalTransformationIdentityNotations. Require Import HoTT.Tactics PathGroupoids Types.Forall.