Proposition enriched_conical_colim_from_coprod_coequalizers_commute (i : I) : enriched_conical_colim_from_coprod_coequalizers_mor · precomp_arr E w (enriched_conical_colim_in_from_coprod_coequalizers i) = fs i. Proof. unfold enriched_conical_colim_from_coprod_coequalizers_mor. unfold enriched_conical_colim_in_from_coprod_coequalizers. rewrite precomp_arr_comp. rewrite !assoc. rewrite (EqualizerCommutes (is_coequalizer_enriched_to_Equalizer E f g enriched_conical_colim_ob_from_coprod_coequalizers_is_coequalizer w)). rewrite (ProductPrCommutes _ _ _ (is_coprod_enriched_to_Product E D is_coprod_tar w)). apply idpath. 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.