C : Type u₁
inst✝ : Category C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (f.app X.op ≫ F.map g.op) (𝟙 X) = f.app Y.op (𝟙 Y ≫ g)
C : Type u₁
inst✝ : Category C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ F.map g.op (↑yonedaEquiv f) = ↑yonedaEquiv (yoneda.map g ≫ f)
change (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)
C : Type u₁
inst✝ : Category C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ ((yoneda.obj X).map g.op ≫ f.app Y.op) (𝟙 X) = f.app Y.op (𝟙 Y ≫ g)
C : Type u₁
inst✝ : Category C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (f.app X.op ≫ F.map g.op) (𝟙 X) = f.app Y.op (𝟙 Y ≫ g)
rw [← f.naturality]
C : Type u₁
inst✝ : Category C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ f.app Y.op (g ≫ 𝟙 X) = f.app Y.op (𝟙 Y ≫ g)
C : Type u₁
inst✝ : Category C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ ((yoneda.obj X).map g.op ≫ f.app Y.op) (𝟙 X) = f.app Y.op (𝟙 Y ≫ g)
dsimp
no goals
C : Type u₁
inst✝ : Category C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ f.app Y.op (g ≫ 𝟙 X) = f.app Y.op (𝟙 Y ≫ g)
simp