Lemma eq_diag_is_eq {C : category} {g : graph} (d d' : diagram g C) : eq_diag d d' -> d = d'. Proof. intros [eqv autreq]. use total2_paths_f. - apply funextfun. intro v. apply eqv. - rewrite (transportf2_comp (λ x y : vertex g → C, ∏ a b : vertex g, edge a b → C ⟦ y a, x b ⟧)). match goal with |- transportf ?Pf ?x1 (transportf ?Pf2 ?s1 ?s2 ) = _ => set (e := x1); set (P := Pf); set (P2 := Pf2); set (tp2:=transportf P2 s1 s2); set (trp := transportf P x1 tp2) end. change (trp = pr2 d'). unfold trp. apply funextsec. intro v; apply funextsec; intro v'. apply funextsec; intro ed. specialize (autreq v v' ed). rewrite <- (pathsinv0inv0 (eqv v)) in autreq. apply pathsinv0 in autreq. apply transportf_transpose_right in autreq. unfold dmor in autreq. rewrite autreq. rewrite pathsinv0inv0. etrans. eapply pathsinv0. apply ( transport_map (P:=P) (Q:=_) (λ x tp, tp v v' ed)). etrans. apply (transportf_funextfun (λ x, C⟦ pr1 d' v,x⟧)). apply maponpaths. etrans. eapply pathsinv0. apply ( transport_map (P:=P2) (Q:=_) (λ x tp, tp v v' ed)). apply (transportf_funextfun (λ x, C⟦ x,pr1 d v'⟧)). 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.