Lemma eq_diag_iscolimcocone: ∏ {C : category} {g : graph} {d : diagram g C} (d' : diagram g C) (eq_d : eq_diag d d') {c : C} {cc:cocone d c} (islimcone : isColimCocone _ _ cc) , isColimCocone _ _ (make_eq_diag_cocone d' eq_d cc). Proof. intros. destruct eq_d as [eq_d1 eq_d2]. set (eq_d := eq_d1,,eq_d2). set (eq_d'' := sym_eq_diag _ _ eq_d). set (eq_d1' := pr1 eq_d''). set (eq_d2' := pr2 eq_d''). set (eq_d' := (eq_d1',,eq_d2'):eq_diag d' d). red. intros c' cc'. set (cc'2 := make_eq_diag_cocone _ 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. rewrite <- (pathsinv0inv0 (eq_d1 v)). eapply pathsinv0. apply transport_source_precompose. etrans. apply maponpaths. apply islim. cbn. now apply (transportbfinv ( (λ x' : C, C ⟦ x', c' ⟧) )). - intro y. apply impred_isaprop. intro t. apply homset_property. - intros y hy. apply (path_to_ctr _ _ islimcone). intro v; specialize (hy v). revert hy. cbn. intro hy. apply (transportf_transpose_right (P:=(λ obj : C, C ⟦ obj, c' ⟧))). etrans. apply transport_source_precompose. unfold transportb. rewrite pathsinv0inv0. apply hy. 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.