proposition: Lemma comma_category_projection_functor_identity_of x : comma_category_projection_functor_morphism_of (Category.Core.identity x) = 1.
proof: Proof. apply CommaCategory.path_morphism; simpl; [ | reflexivity ]. path_functor. exists (path_forall _ _ (comma_category_induced_functor_object_of_identity _)). comma_laws_t. Qed.
imports: Category.Core Functor.Core Category.Prod Functor.Prod.Core Category.Dual Functor.Dual Functor.Composition.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors NatCategory FunctorCategory.Core Cat.Core Functor.Paths Comma.InducedFunctors Comma.Projection Types.Forall PathGroupoids HoTT.Tactics