∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] (F : CategoryTheory.Functor C (Type u_2))
  [inst_1 : CategoryTheory.FunctorToTypes.Small.{u_1, u_2, u_3, u_4} F] (X : C),
  ⇑(equivShrink (F.obj X)) ∘ F.map (CategoryTheory.CategoryStruct.id X) ∘ ⇑(equivShrink (F.obj X)).symm =
    CategoryTheory.CategoryStruct.id (Shrink.{u_1, u_2} (F.obj X))