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.
Mathlib.CategoryTheory.Closed.Types
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.