proposition: Proposition QuiverHomomorphismEquivalence_Transitive (Q Q' : Quiver) : Transitive (QuiverHomomorphismEquivalence Q Q').
proof: Proof. intros F G H [F_eq_G_on_obj FG_coherent_transport] [G_eq_H_on_obj GH_coherent_transport]. unfold QuiverHomomorphismEquivalence in *. exists (fun x => eq_trans (F_eq_G_on_obj x) (G_eq_H_on_obj x)). intros c c' f. unfold Logic.transport_r. rewrite eq_trans_sym_distr. rewrite <- 2! transport_trans. rewrite (FG_coherent_transport c c' f). unfold Logic.transport_r in *. rewrite <- (GH_coherent_transport c c' f). rewrite transport_relation_exchange. reflexivity. Qed.
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