case w.w.h
A : Type u_1
A' : Type u_5
B : Type u_4
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X = (equivalence₂UnitIso eB hF).hom.app X
A : Type u_1
A' : Type u_5
B : Type u_4
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF
ext X
case w.w.h
A : Type u_1
A' : Type u_5
B : Type u_4
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ (equivalence₁ hF).unitIso.hom.app X ≫ (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) =
    (equivalence₂UnitIso eB hF).hom.app X
case w.w.h
A : Type u_1
A' : Type u_5
B : Type u_4
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X = (equivalence₂UnitIso eB hF).hom.app X
dsimp [equivalence₂]
case w.w.h
A : Type u_1
A' : Type u_5
B : Type u_4
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) =
    eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X)))
case w.w.h
A : Type u_1
A' : Type u_5
B : Type u_4
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ (equivalence₁ hF).unitIso.hom.app X ≫ (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) =
    (equivalence₂UnitIso eB hF).hom.app X
simp only [equivalence₂UnitIso_hom_app, equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app,
    assoc, NatIso.cancel_natIso_hom_left]
no goals
case w.w.h
A : Type u_1
A' : Type u_5
B : Type u_4
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) =
    eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X)))
rfl