proposition: Lemma compose_diagonal_functor x (F : Functor D' D) : diagonal_functor C D x o F = diagonal_functor _ _ x.
proof: Proof. path_functor. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core ExponentialLaws.Law1.Functors FunctorCategory.Core KanExtensions.Core InitialTerminalCategory.Core NatCategory Functor.Paths