Proposition enriched_conical_colim_eq_from_coprod_coequalizers {i j : I} (k : i --> j) : # D k · enriched_conical_colim_in_from_coprod_coequalizers i = enriched_conical_colim_in_from_coprod_coequalizers j. Proof. unfold enriched_conical_colim_in_from_coprod_coequalizers. rewrite !assoc. rewrite <- enriched_conical_colim_from_coprod_coequalizers_r_in. rewrite <- (enriched_conical_colim_from_coprod_coequalizers_l_in k). rewrite !assoc'. apply maponpaths. refine (!_). exact (enriched_coequalizer_cocone_eq _ _ _ (pr1 (EE _ _ f g))). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers. Import MonoidalNotations.