Definition self_enriched_is_coprod_weq {w z : V} (f : ∏ (j : J), z --> D j ⊸ w) : (∑ (fs : z --> coprod ⊸ w), ∏ (j : J), fs · precomp_arr (self_enrichment V) w (internal_to_arr (ι j)) = f j) ≃ (∑ (fs : z ⊗ coprod --> w), ∏ (j : J), identity z #⊗ CoproductIn _ _ coprod j · fs = f j #⊗ identity _ · internal_eval (D j) w). Proof. use weqtotal2. - exact (internal_hom_equiv z coprod w). - intro fs ; cbn -[ι]. use weqonsecfibers. intro j. apply self_enriched_is_coprod_weq_path. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedInitial. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedBinaryCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. 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.Preservation. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Import MonoidalNotations.