V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (lift φ).map (Quiver.Hom.toPath f) = φ.map f
dsimp [Quiver.Hom.toPath, lift]
no goals
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
simp