Theorems · Inductive type · category theory

CategoryTheory.Functor.RepresentableBy

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᵒᵖ (Type v) → C → Type (max (max u₁ v) v₁)

The data which expresses that a functor F : Cᵒᵖ ⥤ Type v is representable by Y : C. In the situation where F factors through a concrete category, it may be more convenient to use the API in the file Mathlib/CategoryTheory/ConcreteCategory/Representable.lean.

Defined in

Mathlib.CategoryTheory.Yoneda

Cited by

51 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.Category