proposition: Lemma comma_category_induced_functor_object_of_identity s x : comma_category_induced_functor_object_of (Category.Core.identity s) x = x.
proof: 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.
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Dual Category.Prod NaturalTransformation.Identity FunctorCategory.Core Cat.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors HoTT.Tactics Basics.Tactics