Definition is_power_self_enrichment_power_cone : is_power_enriched (self_enrichment V) v₁ v₂ self_enrichment_power_cone. Proof. use make_is_power_enriched. - exact (λ w, internal_swap_arg v₁ v₂ w). - exact is_power_self_enrichment_power_cone_eq_1. - exact is_power_self_enrichment_power_cone_eq_2. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations.