Definition dialgebra_enrichment_data : enrichment_data (dialgebra F G) V. Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (λ f g, dialgebra_enrichment_mor (pr2 f) (pr2 g)). - exact (λ f, dialgebra_enrichment_id (pr2 f)). - exact (λ f₁ f₂ f₃, dialgebra_enrichment_comp (pr2 f₁) (pr2 f₂) (pr2 f₃)). - exact (λ f g τ, dialgebra_enrichment_from_arr (pr1 τ) (pr2 τ)). - refine (λ f g τ, dialgebra_enrichment_to_arr_mor τ ,, _). exact (dialgebra_enrichment_to_arr_eq τ). 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.