proposition: Lemma diagonal_functor_diagonal_functor' X : diagonal_functor X = diagonal_functor' (X (center _)).
proof: Proof. path_functor. simpl. repeat (apply path_forall || intro). apply identity_of. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core ExponentialLaws.Law1.Functors FunctorCategory.Core KanExtensions.Core InitialTerminalCategory.Core NatCategory Functor.Paths