Lemma eq_diag_islimcone: ∏ {C : category} {g : graph} {d : diagram g C} (d' : diagram g C) (eq_d : eq_diag d d') {c : C} {cc:cone d c} (islimcone : isLimCone _ _ cc) , isLimCone _ _ (make_eq_diag_cone d' eq_d cc). Proof. intros. set (eq_d1 := pr1 eq_d); set (eq_d2 := pr1 eq_d). set (eq_d' := sym_eq_diag _ _ eq_d). set (eq_d1' := pr1 eq_d'). set (eq_d2' := pr2 eq_d'). red. intros c' cc'. set (cc'2 := make_eq_diag_cone _ eq_d' cc'). specialize (islimcone c' cc'2). apply (unique_exists (pr1 (pr1 islimcone))). - intro v. assert (islim := is_exists_unique islimcone v). cbn in islim. cbn. etrans. eapply pathsinv0. apply transport_target_postcompose. etrans. apply maponpaths. apply islim. apply transportfbinv. - intro y. apply impred_isaprop. intro t. apply homset_property. - intros y hy. apply (path_to_ctr _ _ islimcone). intro v; specialize (hy v). cbn. apply transportf_transpose_right. rewrite <- hy. etrans. unfold transportb. rewrite pathsinv0inv0. apply transport_target_postcompose. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.