Proposition enriched_conical_lim_eq_from_prod_equalizers {i j : I} (k : i --> j) : enriched_conical_lim_pr_from_prod_equalizers i · # D k = enriched_conical_lim_pr_from_prod_equalizers j. Proof. unfold enriched_conical_lim_pr_from_prod_equalizers. rewrite !assoc'. rewrite <- enriched_conical_lim_from_prod_equalizers_r_pr. rewrite <- (enriched_conical_lim_from_prod_equalizers_l_pr k). rewrite !assoc. apply maponpaths_2. refine (!_). exact (enriched_equalizer_cone_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.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.