∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C}
  {S : CategoryTheory.Sieve X} (z₁ z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S),
  (∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
      CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ =
        CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂) →
    z₁ = z₂