{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {η : F ⟶ A} →
        {μ : G ⟶ A} →
          {X : C} →
            {s : CategoryTheory.yoneda.obj X ⟶ A} →
              CategoryTheory.OverPresheafAux.OverArrows η s →
                (ε : F ⟶ G) → CategoryTheory.CategoryStruct.comp ε μ = η → CategoryTheory.OverPresheafAux.OverArrows μ s