C : Type u₁
inst✝ : Category C
X Y : C
f : X.op ⟶ Y.op
⊢ f.unop ≫ 𝟙 X = 𝟙 Y ≫ f.unop
C : Type u₁
inst✝ : Category C
X Y : C
f : X.op ⟶ Y.op
⊢ (yoneda.obj X).map f (𝟙 X) = (yoneda.map f.unop).app Y.op (𝟙 Y)
dsimp
no goals
C : Type u₁
inst✝ : Category C
X Y : C
f : X.op ⟶ Y.op
⊢ f.unop ≫ 𝟙 X = 𝟙 Y ≫ f.unop
simp