mk_vcomp

Mathlib.CategoryTheory.Bicategory.Free

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

Lean4

@[simp]
theorem mk_vcomp {f g h : a ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h) : (η.vcomp θ).mk = (η.mk ≫ θ.mk : f ⟶ h) :=
  rfl

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

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

Разделы

Аффилиация

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