{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {A : C} → (f g : CategoryTheory.MonoOver A) → (CategoryTheory.MonoOver.inf.obj f).obj g ⟶ f