mk_whisker_left

Mathlib.CategoryTheory.Bicategory.Free

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

Lean4

@[simp]
theorem mk_whisker_left (f : a ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h) :
    (Hom₂.whisker_left f η).mk = (f ◁ η.mk : f ≫ g ⟶ f ≫ h) :=
  rfl

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

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

Разделы

Аффилиация

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