{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} →
          CategoryTheory.Presieve.FamilyOfElements P R → (P ⟶ Q) → CategoryTheory.Presieve.FamilyOfElements Q R