C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ e.functor.map ((unit e).app X) = (counitInv e).app (e.functor.obj X)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ (counitInv e).app (e.functor.obj X) = e.functor.map ((unit e).app X)
symm
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 ((𝟭 D).obj (e.functor.toPrefunctor.1 ((𝟭 C).obj X)))
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ e.functor.map ((unit e).app X) = (counitInv e).app (e.functor.obj X)
erw [← Iso.comp_hom_eq_id (e.counitIso.app _), functor_unit_comp]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 ((𝟭 D).obj (e.functor.toPrefunctor.1 ((𝟭 C).obj X)))
rfl