Proposition enriched_conical_lim_from_prod_equalizers_commute (i : I) : enriched_conical_lim_from_prod_equalizers_mor · postcomp_arr E w (enriched_conical_lim_pr_from_prod_equalizers i) = fs i. Proof. unfold enriched_conical_lim_from_prod_equalizers_mor. unfold enriched_conical_lim_pr_from_prod_equalizers. rewrite postcomp_arr_comp. rewrite !assoc. rewrite (EqualizerCommutes (is_equalizer_enriched_to_Equalizer E f g enriched_conical_lim_ob_from_prod_equalizers_is_equalizer w)). rewrite (ProductPrCommutes _ _ _ (is_prod_enriched_to_Product E D is_prod_src 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.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.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Import MonoidalNotations.