# mathlibdocumentation

category_theory.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.

@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.functor.cartesian_closed {C : Type v₁}  :
Equations