MonoidalSingleObj

Mathlib.CategoryTheory.Bicategory.SingleObj

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

Lean4

/-- Promote a monoidal category to a bicategory with a single object.
(The objects of the monoidal category become the 1-morphisms,
with composition given by tensor product,
and the morphisms of the monoidal category become the 2-morphisms.)
-/
@[nolint unusedArguments]
def MonoidalSingleObj (C : Type u) [Category.{v} C] [MonoidalCategory C] :=
  Unit
deriving Inhabited

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

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

Разделы

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

Аффилиация

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