s d d' (m : morphism ((A -> C)^op * (B -> C)) d d') (m' : morphism ((A -> C)^op * (B -> C)) s d) x : comma_category_induced_functor_object_of (m o m') x = comma_category_induced_functor_object_of m (comma_category_induced_functor_object_of m' x). Proof. let x1 := match goal with |- ?x1 = ?x2 => constr:(x1) end in let x2 := match goal with |- ?x1 = ?x2 => constr:(x2) end in apply (CommaCategory.path_object' x1 x2 idpath idpath). abstract ( destruct m', m, x; simpl in *; rewrite !associativity; 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.