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.

    This is not a good instance because of the universe levels. Below is the instance where the target category is Type (max u₁ v₁).

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