homCategory

Mathlib.CategoryTheory.Bicategory.Free

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

Lean4

instance homCategory (a b : FreeBicategory B) : Category (a ⟶ b)
    where
  Hom f g := Quot (@Rel _ _ a b f g)
  id f := Quot.mk Rel (Hom₂.id f)
  comp := @fun _ _ _ => Quot.map₂ Hom₂.vcomp Rel.vcomp_right Rel.vcomp_left
  id_comp := by
    rintro f g ⟨η⟩
    exact Quot.sound (Rel.id_comp η)
  comp_id := by
    rintro f g ⟨η⟩
    exact Quot.sound (Rel.comp_id η)
  assoc := by
    rintro f g h i ⟨η⟩ ⟨θ⟩ ⟨ι⟩
    exact Quot.sound (Rel.assoc η θ ι)

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

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

Разделы

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

Аффилиация

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