s x : comma_category_induced_functor_object_of (Category.Core.identity s) x = 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). simpl. abstract (rewrite ?left_identity, ?right_identity; 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.