Lemma sym_eq_diag {C : category} {g : graph} (d d' : diagram g C) : eq_diag d d' -> eq_diag d' d. Proof. intros eq_d. set (eq_d1 := pr1 eq_d). set (eq_d2 := pr2 eq_d). use tpair. - intro v. apply (! (eq_d1 v)). - unfold eq_d1. assert (heqdag:eq_diag d' d). + apply eq_is_eq_diag. apply pathsinv0. apply eq_diag_is_eq. assumption. + abstract (cbn; intros v v' f; specialize (eq_d2 v v' f); apply pathsinv0; unfold transportb; rewrite pathsinv0inv0; apply (transportf_transpose_right (P:=(λ obj : C, C ⟦ obj, dob d' v' ⟧))); assert (eq_d2':=transportf_transpose_right (P:=(precategory_morphisms (dob d' v))) (! eq_d2)); rewrite eq_d2'; unfold transportb; rewrite pathsinv0inv0; apply (transport_swap (λ a b, C⟦b,a⟧))). Defined.
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.