Documentation

Mathlib.CategoryTheory.Closed.Types

Cartesian closure of Type #

Show that Type u₁ is cartesian closed, and C ⥤ Type u₁ is cartesian closed for C a small category in Type u₁. Note this implies that the category of presheaves on a small category C is cartesian closed.

The adjunction Limits.Types.binaryProductFunctor.obj X ⊣ coyoneda.obj (Opposite.op X) for any X : Type v₁.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.