∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (x : CategoryTheory.AsSmall C),
  (CategoryTheory.AsSmall.down.comp CategoryTheory.AsSmall.up).obj x =
    (CategoryTheory.Functor.id (CategoryTheory.AsSmall C)).obj x