YonedaCollection — Mathlib

Lean4
/-- To give an object of `Over A`, we will in particular need a presheaf `Cᵒᵖ ⥤ Type v`. This is the
definition of that presheaf on objects.

We would prefer to think of this sigma type to be indexed by natural transformations
`yoneda.obj X ⟶ A` instead of `A.obj (op X)`. These are equivalent by the Yoneda lemma, but
we cannot use the former because that type lives in the wrong universe. Hence, we will provide
a lot of API that will enable us to pretend that we are really indexing over
`yoneda.obj X ⟶ A`. -/
def YonedaCollection (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (X : C) : Type v :=
  Σ s : A.obj (op X), F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm s)))
Похожие утверждения