proposition: Lemma comma_category_projection_functor_composition_of s d d' m m' : comma_category_projection_functor_morphism_of (@Category.Core.compose _ s d d' m' m) = (comma_category_projection_functor_morphism_of m') o (comma_category_projection_functor_morphism_of m).
proof: Proof. apply CommaCategory.path_morphism; simpl; [ | reflexivity ]. path_functor. simpl. exists (path_forall _ _ (comma_category_induced_functor_object_of_compose m' m)). 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