C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
Y : D
⊢ e.inverse.map ((counit e).app Y) = (unitInv e).app (e.inverse.obj Y)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
Y : D
⊢ (unitInv e).app (e.inverse.obj Y) = e.inverse.map ((counit e).app Y)
symm
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 ((𝟭 C).obj (e.inverse.obj Y))
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
Y : D
⊢ e.inverse.map ((counit e).app Y) = (unitInv e).app (e.inverse.obj Y)
erw [← Iso.hom_comp_eq_id (e.unitIso.app _), 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) = 𝟙 ((𝟭 C).obj (e.inverse.obj Y))
rfl