∀ {A : Type u_1} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} B] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'}
  {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (η : G.comp F ≅ eB.functor) (X : B),
  (AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso η).inv.app X =
    CategoryTheory.CategoryStruct.comp (eB.unitIso.hom.app X) (eB.inverse.map (η.inv.app X))