Cartesian closure of Type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[protected, instance]

def category_theory.obj.is_left_adjoint (X : Type v₁) :

category_theory.is_left_adjoint (category_theory.limits.types.binary_product_functor.obj X)

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' := _}}

source

@[protected, instance]

def category_theory.sort.limits.has_finite_products :

category_theory.limits.has_finite_products (Type v₁)

source

@[protected, instance]

noncomputable def category_theory.sort.cartesian_closed :

category_theory.cartesian_closed (Type v₁)

Equations

category_theory.sort.cartesian_closed = {closed' := λ (X : Type v₁), {is_adj := category_theory.adjunction.left_adjoint_of_nat_iso (category_theory.limits.types.binary_product_iso_prod.app X) (category_theory.obj.is_left_adjoint X)}}

source

@[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₁)

source

@[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)}}