instCartesianClosedFunctorType — Mathlib

Lean4

instance {C : Type v₁} [SmallCategory C] : CartesianClosed (C ⥤ Type v₁) :=
  CartesianClosed.mk _ fun F =>
    by
    haveI : ∀ X : Type v₁, PreservesColimits (tensorLeft X) := by infer_instance
    letI : PreservesColimits (tensorLeft F) := ⟨by infer_instance⟩
    have := Presheaf.isLeftAdjoint_of_preservesColimits.{v₁} (tensorLeft F)
    exact
      Exponentiable.mk _ _
        (Adjunction.ofIsLeftAdjoint (tensorLeft F))
          -- TODO: once we have `MonoidalClosed` instances for functor categories into general monoidal
          -- closed categories, replace this with that, as it will be a more explicit construction.

Похожие утверждения