∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C)
  (x : F.obj (Opposite.op X)),
  CategoryTheory.OverPresheafAux.unitBackward η X x =
    CategoryTheory.OverPresheafAux.YonedaCollection.mk (CategoryTheory.yonedaEquiv.symm (η.app (Opposite.op X) x))
      ⟨x, ⋯⟩