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
- category_theory.obj.is_left_adjoint X = {right := {obj := λ (Y : Type v₁), X ⟶ Y, map := λ (Y₁ Y₂ : Type v₁) (f : Y₁ ⟶ Y₂) (g : X ⟶ Y₁), g ≫ f, map_id' := _, map_comp' := _}, adj := category_theory.adjunction.mk_of_unit_counit {unit := {app := λ (Z : Type v₁) (z : Z) (x : X), (x, z), naturality' := _}, counit := {app := λ (Z : Type v₁) (xf : ({obj := λ (Y : Type v₁), X ⟶ Y, map := λ (Y₁ Y₂ : Type v₁) (f : Y₁ ⟶ Y₂) (g : X ⟶ Y₁), g ≫ f, map_id' := _, map_comp' := _} ⋙ category_theory.limits.types.binary_product_functor.obj X).obj Z), xf.snd xf.fst, naturality' := _}, left_triangle' := _, right_triangle' := _}}
@[protected, instance]
@[protected, instance]
noncomputable
def
category_theory.sort.cartesian_closed
:
category_theory.cartesian_closed (Type v₁)
Equations
@[protected, instance]
def
category_theory.functor.limits.has_finite_products
{C : Type u₁}
[category_theory.category C] :
category_theory.limits.has_finite_products (C ⥤ Type u₁)
@[protected, instance]
noncomputable
def
category_theory.functor.cartesian_closed
{C : Type v₁}
[category_theory.small_category C] :
category_theory.cartesian_closed (C ⥤ Type v₁)
Equations
- category_theory.functor.cartesian_closed = {closed' := λ (F : C ⥤ Type v₁), {is_adj := let _inst : category_theory.limits.preserves_colimits (category_theory.limits.prod.functor.obj F) := category_theory.functor_category.prod_preserves_colimits F in category_theory.is_left_adjoint_of_preserves_colimits (category_theory.limits.prod.functor.obj F)}}