∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.LocallySmall.{u_2, u_3, u_1} C]
  {X Y : CategoryTheory.ShrinkHoms.{u_1} C} (f : Shrink.{u_2, u_3} (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)),
  (equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms))
      (CategoryTheory.CategoryStruct.comp
        ((equivShrink (X.fromShrinkHoms ⟶ X.fromShrinkHoms)).symm
          ((equivShrink (X.fromShrinkHoms ⟶ X.fromShrinkHoms)) (CategoryTheory.CategoryStruct.id X.fromShrinkHoms)))
        ((equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)).symm f)) =
    f