curry_id_eq_coev

Mathlib.CategoryTheory.Closed.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalClosed.curry_id_eq_coev

English

Curry of the identity on A ⊗ X equals the coevaluation at A applied to X.

Русский

Карри тождества на A ⊗ X равняется коеволюции в A применённой к X.

LaTeX

$$$\mathrm{curry}(\mathrm{id}_{A \otimes X}) = (\mathrm{ihom.coev} A).app X$$$

Lean4

theorem curry_id_eq_coev : curry (𝟙 _) = (ihom.coev A).app X :=
  by
  rw [curry_eq, (ihom A).map_id (A ⊗ _)]
  apply comp_id

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

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

Разделы

Аффилиация

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