{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) →
      [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)] →
        CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.id X) ≅
          CategoryTheory.Functor.id (CategoryTheory.Over X)