Definition self_enriched_is_coequalizer_weq {w z : V} (h : z --> y ⊸ w) (r : h · precomp_arr (self_enrichment V) w f = h · precomp_arr (self_enrichment V) w g) : (∑ (φ : z --> c ⊸ w), φ · precomp_arr (self_enrichment V) w (internal_to_arr (internal_from_arr e)) = h) ≃ (∑ (φ : z ⊗ c --> w), identity z #⊗ CoequalizerArrow c · φ = h #⊗ identity _ · internal_eval y w). Proof. use weqtotal2. - exact (internal_hom_equiv z c w). - exact (self_enriched_is_coequalizer_path_weq h). 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.