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.
def
CategoryTheory.Types.binaryProductAdjunction
(X : Type v₁)
:
CategoryTheory.Limits.Types.binaryProductFunctor.obj X ⊣ CategoryTheory.coyoneda.obj { unop := X }
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
instance
CategoryTheory.instIsLeftAdjointObjFunctorTypeBinaryProductFunctor
(X : Type v₁)
:
(CategoryTheory.Limits.Types.binaryProductFunctor.obj X).IsLeftAdjoint
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.instHasFiniteProductsFunctorType
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.instCartesianClosedFunctorType
{C : Type v₁}
[CategoryTheory.SmallCategory C]
:
Equations
- One or more equations did not get rendered due to their size.