{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) →
      {W X B : C} →
        (f : X ⟶ B) →
          (g₁ g₂ : W ⟶ X) →
            CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
              P.obj (Opposite.op B) → ↑{x | P.map g₁.op x = P.map g₂.op x}