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

@[instance]
Equations
@[instance]
@[instance]
Equations
@[instance]
Equations