{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : Type (max u₁ u₂)) →
      [Unique X] →
        CategoryTheory.Functor.sectionsFunctor C ≅
          CategoryTheory.coyoneda.obj (Opposite.op ((CategoryTheory.Functor.const C).obj X))