coev

Mathlib.CategoryTheory.Closed.Cartesian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.exp.coev

Lean4

/-- The coevaluation natural transformation. -/
abbrev coev : 𝟭 C ⟶ tensorLeft A ⋙ exp A :=
  ihom.coev A

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

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

Разделы

Аффилиация

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