s d m s0 d0 (m0 : morphism (fst s / snd s) s0 d0) : morphism (fst d / snd d) (@comma_category_induced_functor_object_of s d m s0) (@comma_category_induced_functor_object_of s d m d0). Proof. simpl. let s := match goal with |- CommaCategory.morphism ?s ?d => constr:(s) end in let d := match goal with |- CommaCategory.morphism ?s ?d => constr:(d) end in refine (CommaCategory.Build_morphism s d (CommaCategory.g m0) (CommaCategory.h m0) _); simpl in *; clear. abstract ( destruct_head prod; destruct_head CommaCategory.morphism; destruct_head CommaCategory.object; simpl in *; repeat (try_associativity_quick (rewrite <- !commutes || (progress f_ap))); repeat (try_associativity_quick (rewrite !commutes || (progress f_ap))); assumption ). 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.