Definition make_self_enriched_is_coequalizer : is_coequalizer_enriched (self_enrichment V) f g make_self_enriched_coequalizer_cocone. Proof. intros w z h r. use (iscontrweqb (self_enriched_is_coequalizer_weq h r)). refine (left_adjoint_preserves_coequalizer _ (sym_mon_closed_left_tensor_left_adjoint V z) _ _ _ _ _ _ _ _ (pr22 c) _ _ _). - cbn. rewrite <- !tensor_comp_id_l. apply maponpaths. apply CoequalizerEqAr. - abstract (cbn ; pose (maponpaths (λ z, z #⊗ identity _ · internal_eval _ _) r) as r' ; cbn in r' ; rewrite !self_enrichment_precomp in r' ; rewrite !tensor_comp_id_r in r' ; rewrite !assoc' in r' ; rewrite !internal_beta in r' ; rewrite !assoc in r' ; rewrite <- !tensor_split' in r' ; rewrite !assoc ; rewrite <- !tensor_split ; exact r'). 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.