s d (m : morphism ((A -> C)^op * (B -> C)) s d) : Functor (fst s / snd s) (fst d / snd d). Proof. refine (Build_Functor (fst s / snd s) (fst d / snd d) (@comma_category_induced_functor_object_of s d m) (@comma_category_induced_functor_morphism_of s d m) _ _ ); abstract ( intros; apply CommaCategory.path_morphism; reflexivity ). Defined.
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.