C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 (e.inverse.obj ((𝟭 D).obj Y))
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
Y : D
⊢ (unit e).app (e.inverse.obj Y) = e.inverse.map ((counitInv e).app Y)
erw [← Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)), unit_inverse_comp]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 (e.inverse.obj ((𝟭 D).obj Y))
dsimp