fact: Definition QuiverHomomorphismEquivalence (Q : Quiver) (Q' : Quiver) (F G : QuiverHomomorphism Q Q') : Type := { node_equiv : forall x : Q, (@fnodes _ _ F x) = (@fnodes _ _ G x) & forall (x y : Q) (f : edges x y), let eqx := node_equiv x in let eqy := node_equiv y in let Ff := @fedgemap _ _ F x y f in let Gf := @fedgemap _ _ G x y f in (Logic.transport (fun t => edges (F x) t) eqy Ff ≈ Logic.transport_r (fun t => edges t (G y)) eqx Gf) }.
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