∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) [inst_1 : R.HasPairwisePullbacks],
  CategoryTheory.Equalizer.Presieve.firstMap P R =
    CategoryTheory.Limits.Pi.lift fun fg =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) fg.1)
        (P.map (CategoryTheory.Limits.pullback.fst ↑fg.1.snd ↑fg.2.snd).op)