categoryStruct

Mathlib.CategoryTheory.Bicategory.Free

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FreeBicategory.categoryStruct

Lean4

instance categoryStruct : CategoryStruct.{max u v} (FreeBicategory B)
    where
  id := fun a : B => Hom.id a
  comp := @fun _ _ _ => Hom.comp

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

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

Разделы

Аффилиация

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