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.

instance CategoryTheory.instIsLeftAdjointTypeTypesObjToQuiverToCategoryStructFunctorToQuiverToCategoryStructCategoryToPrefunctorBinaryProductFunctor (X : Type v₁) : CategoryTheory.IsLeftAdjoint (CategoryTheory.Limits.Types.binaryProductFunctor.obj X)

Equations

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

instance CategoryTheory.instHasFiniteProductsTypeTypes : CategoryTheory.Limits.HasFiniteProducts (Type v₁)

Equations

• CategoryTheory.instHasFiniteProductsTypeTypes = ⋯

instance CategoryTheory.instCartesianClosedTypeTypesInstHasFiniteProductsTypeTypes : CategoryTheory.CartesianClosed (Type v₁)

Equations

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

instance CategoryTheory.instHasFiniteProductsFunctorTypeTypesCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Functor C (Type u₂))

Equations

• ⋯ = ⋯

instance CategoryTheory.instCartesianClosedFunctorTypeTypesCategoryInstHasFiniteProductsFunctorTypeTypesCategory {C : Type v₁} [CategoryTheory.SmallCategory C] : CategoryTheory.CartesianClosed (CategoryTheory.Functor C (Type v₁))

Equations

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