proposition: Proposition QuiverHomomorphismEquivalence_Symmetric (Q Q' : Quiver) : Symmetric (QuiverHomomorphismEquivalence Q Q').
proof: Proof. intros F G [F_eq_G_on_obj FG_coherent_transport]. simpl in FG_coherent_transport. exists (fun x => eq_sym (F_eq_G_on_obj x)). simpl. intros c c' f. unfold Logic.transport_r in *. rewrite eq_sym_involutive. specialize FG_coherent_transport with c c' f. apply (proper_transport_dom Q' edges _ (F c) (G c) (G c') (F_eq_G_on_obj c)) in FG_coherent_transport. rewrite transport_trans, eq_trans_sym_inv_l in FG_coherent_transport; simpl in FG_coherent_transport. apply (proper_transport_cod Q' edges _ (G c) (G c') (F c') (eq_sym (F_eq_G_on_obj c'))) in FG_coherent_transport. rewrite transport_relation_exchange, transport_trans, eq_trans_sym_inv_r in FG_coherent_transport; simpl in FG_coherent_transport. symmetry; exact FG_coherent_transport. Defined.
imports: Category.Lib Category.Lib.TList Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Adjunction Category.Theory.Universal.Arrow Category.Instance.StrictCat Category.Construction.Groupoid Category.Construction.Opposite Category.Construction.Product Category.Instance.Sets