Hom

Mathlib.CategoryTheory.Bicategory.Free

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

Lean4

/-- 1-morphisms in the free bicategory. -/
inductive Hom : B → B → Type max u v
  | of {a b : B} (f : a ⟶ b) : Hom a b
  | id (a : B) : Hom a a
  | comp {a b c : B} (f : Hom a b) (g : Hom b c) : Hom a c

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

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

Разделы

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

Аффилиация

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