Functors to Type are closed.

Show that C ⥤ Type max w v u is monoidal closed for C a category in Type u with morphisms in Type v, and w an arbitrary universe.

TODO

It should be shown that C ⥤ Type max w v u is Cartesian closed.

def CategoryTheory.FunctorToTypes.functorHomEquiv {C : Type u} [Category.{v, u} C] (F G H : Functor C (Type (max w v u))) : (G ⟶ F.functorHom H) ≃ (MonoidalCategoryStruct.tensorObj F G ⟶ H)

When F G H : C ⥤ Type max w v u, we have (G ⟶ F.functorHom H) ≃ (F ⊗ G ⟶ H).

Equations

• CategoryTheory.FunctorToTypes.functorHomEquiv F G H = (F.functorHomEquiv H G).trans (F.homObjEquiv H G)

@[simp]

theorem CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app {C : Type u} [Category.{v, u} C] (F G H : Functor C (Type (max w v u))) (a✝ : MonoidalCategoryStruct.tensorObj F G ⟶ H) (X : C) : ((functorHomEquiv F G H).symm a✝).app X = TypeCat.ofHom fun (a : G.obj X) => { app := fun (Y : C) (f : X ⟶ Y) => TypeCat.ofHom fun (x : F.obj Y) => (ConcreteCategory.hom (a✝.app Y)) (x, (ConcreteCategory.hom (G.map f)) a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app {C : Type u} [Category.{v, u} C] (F G H : Functor C (Type (max w v u))) (a✝ : G ⟶ F.functorHom H) (X : C) : ((functorHomEquiv F G H) a✝).app X = TypeCat.ofHom fun (x : MonoidalCategoryStruct.tensorObj (F.obj X) (G.obj X)) => match x with | (x, y) => (ConcreteCategory.hom (((ConcreteCategory.hom (a✝.app X)) y).app X (CategoryStruct.id X))) x

def CategoryTheory.FunctorToTypes.rightAdj {C : Type u} [Category.{v, u} C] (F : Functor C (Type (max w v u))) : Functor (Functor C (Type (max w v u))) (Functor C (Type (max w v u)))

A right adjoint of tensorLeft F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.rightAdj_map_app {C : Type u} [Category.{v, u} C] (F : Functor C (Type (max w v u))) {X✝ Y✝ : Functor C (Type (max w v u))} (f : X✝ ⟶ Y✝) (X : C) : ((rightAdj F).map f).app X = TypeCat.ofHom fun (a : F.HomObj X✝ (coyoneda.obj (Opposite.op X))) => { app := fun (d : C) (b : X ⟶ d) => CategoryStruct.comp (a.app d b) (f.app d), naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.rightAdj_obj_map {C : Type u} [Category.{v, u} C] (F G : Functor C (Type (max w v u))) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((rightAdj F).obj G).map f = TypeCat.ofHom fun (x : F.HomObj G (coyoneda.obj (Opposite.op X✝))) => { app := fun (X : C) (a : Y✝ ⟶ X) => x.app X (CategoryStruct.comp f a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.rightAdj_obj_obj {C : Type u} [Category.{v, u} C] (F G : Functor C (Type (max w v u))) (X : C) : ((rightAdj F).obj G).obj X = F.HomObj G (coyoneda.obj (Opposite.op X))

@[deprecated CategoryTheory.FunctorToTypes.rightAdj "Use `(rightAdj F).map instead" (since := "2026-04-08")]

def CategoryTheory.FunctorToTypes.rightAdj_map {C : Type u} [Category.{v, u} C] (F : Functor C (Type (max w v u))) : Functor (Functor C (Type (max w v u))) (Functor C (Type (max w v u)))

Alias of CategoryTheory.FunctorToTypes.rightAdj.

---

A right adjoint of tensorLeft F.

Equations

• @CategoryTheory.FunctorToTypes.rightAdj_map = @CategoryTheory.FunctorToTypes.rightAdj

def CategoryTheory.FunctorToTypes.adj {C : Type u} [Category.{v, u} C] (F : Functor C (Type (max w v u))) : MonoidalCategory.tensorLeft F ⊣ rightAdj F

The adjunction tensorLeft F ⊣ rightAdj F.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CategoryTheory.FunctorToTypes.closed {C : Type u} [Category.{v, u} C] (F : Functor C (Type (max w v u))) : Closed F

Equations

• CategoryTheory.FunctorToTypes.closed F = { rightAdj := CategoryTheory.FunctorToTypes.rightAdj F, adj := CategoryTheory.FunctorToTypes.adj F }

@[implicit_reducible]

instance CategoryTheory.FunctorToTypes.monoidalClosed {C : Type u} [Category.{v, u} C] : MonoidalClosed (Functor C (Type (max w v u)))

Equations

• CategoryTheory.FunctorToTypes.monoidalClosed = { closed := inferInstance }