∀ {V : Type u} [inst : Quiver V] (left right : V) (hom : left ⟶ right) (left_1 right_1 : V) (hom_1 : left_1 ⟶ right_1),
  ({ left := left, right := right, hom := hom } = { left := left_1, right := right_1, hom := hom_1 }) =
    (left = left_1 ∧ right = right_1 ∧ hom ≍ hom_1)