∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) (a : CategoryTheory.Presieve.FamilyOfElements P R),
  (CategoryTheory.Equalizer.firstObjEqFamily P R).inv a = CategoryTheory.Limits.Pi.lift (fun f x => x ↑f.snd ⋯) a