∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (f : X ⟶ Y) (x : P.obj (Opposite.op X)), (CategoryTheory.Presieve.FamilyOfElements.singletonEquiv P f).symm x f ⋯ = x