cartesianClosedFunctorToTypes

Mathlib.CategoryTheory.Closed.Types

URI: https://scilib.ai/kg/mathlib#CategoryTheory.cartesianClosedFunctorToTypes

Lean4

/-- This is not a good instance because of the universe levels. Below is the instance where the
target category is `Type (max u₁ v₁)`. -/
def cartesianClosedFunctorToTypes {C : Type u₁} [Category.{v₁} C] : CartesianClosed (C ⥤ Type (max u₁ v₁ u₂)) :=
  let e : (ULiftHom.{max u₁ v₁ u₂} (ULift.{max u₁ v₁ u₂} C)) ⥤ Type (max u₁ v₁ u₂) ≌ C ⥤ Type (max u₁ v₁ u₂) :=
    Functor.asEquivalence ((Functor.whiskeringLeft _ _ _).obj (ULift.equivalence.trans ULiftHom.equiv).functor)
  cartesianClosedOfEquiv e

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru