Definition nat_trans_to_dialgebra_enrichment : functor_enrichment (nat_trans_to_dialgebra K τ) E₀ dialgebra_enrichment. Proof. simple refine (_ ,, _). - exact nat_trans_to_dialgebra_enrichment_mor. - repeat split. + abstract (intros x ; use dialgebra_enrichment_mor_eq_of_mor ; cbn ; rewrite !assoc' ; rewrite nat_trans_to_dialgebra_enrichment_mor_incl ; rewrite dialgebra_enrichment_id_incl ; apply (functor_enrichment_id EK)). + abstract (intros x y z ; use dialgebra_enrichment_mor_eq_of_mor ; cbn ; rewrite !assoc' ; rewrite nat_trans_to_dialgebra_enrichment_mor_incl ; rewrite dialgebra_enrichment_comp_incl ; refine (functor_enrichment_comp EK x y z @ _) ; unfold dialgebra_enrichment_comp_mor ; rewrite !assoc ; apply maponpaths_2 ; refine (_ @ tensor_comp_mor _ _ _ _) ; rewrite !nat_trans_to_dialgebra_enrichment_mor_incl ; apply idpath). + abstract (intros x y f ; use dialgebra_enrichment_mor_eq_of_mor ; cbn ; rewrite !assoc' ; rewrite nat_trans_to_dialgebra_enrichment_mor_incl ; rewrite dialgebra_enrichment_from_arr_incl ; apply (functor_enrichment_from_arr EK)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Limits.Equalizers. Import MonoidalNotations.