comp

Mathlib.CategoryTheory.Monoidal.NaturalTransformation

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.IsMonoidal.comp

Русский

Идентичность естественного преобразования 𝟙F является моноидальной для любого F с лаксомонодальной структурой.

LaTeX

$$$\\text{IsMonoidal}(\\mathbf{1}_F)$$$

Lean4

instance comp (τ' : F₂ ⟶ F₃) [IsMonoidal τ] [IsMonoidal τ'] : IsMonoidal (τ ≫ τ') where

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

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

Разделы

Аффилиация

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