U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq e e'
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ Hom.cast (_ : v = v') (_ : w = w) e = e'
rw [Hom.cast_eq_iff_heq]
no goals
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq e e'
exact hom_heq_of_cons_eq_cons h