instCartesianClosedType

Mathlib.CategoryTheory.Closed.Types

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

Lean4

instance : CartesianClosed (Type v₁) :=
  CartesianClosed.mk _ fun X => Exponentiable.mk _ _ (Types.tensorProductAdjunction X)

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

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

Разделы

Аффилиация

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