s d (m : morphism (S / T) s d) : morphism (S' / T') (functorial_morphism_of_object_of s) (functorial_morphism_of_object_of d). Proof. simpl in *. refine (CommaCategory.Build_morphism (functorial_morphism_of_object_of s) (functorial_morphism_of_object_of d) (AF _1 (CommaCategory.g m)) (BF _1 (CommaCategory.h m)) _). unfold functorial_morphism_of_object_of; simpl. clear. abstract helper (exact (CommaCategory.p m)) (commutes TA) (commutes TB). 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.