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