proposition: Proposition self_enrichment_laws : enrichment_laws self_enrichment_data.
proof: Proof. repeat split. - exact internal_id_left. - exact internal_id_right. - exact internal_assoc. - exact (@internal_to_from_arr V). - exact (@internal_from_to_arr V). - exact internal_to_arr_id. - exact (@internal_to_arr_comp V). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.StrongMonad UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed