hComp_id_heq

Mathlib.CategoryTheory.Bicategory.CatEnriched

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatEnrichedOrdinary.hComp_id_heq

English

The HEq version of the left-unit law holds: hComp η (𝟙 (𝟙 b)) is HEq to η.

Русский

HEq-версия левого единичного закона: hComp η (𝟙 (𝟙 b)) эквивалентно η.

LaTeX

$$$HEq( hComp(\\eta, \\mathbf{1}(\\mathbf{1} b)), η)$$$

Lean4

theorem hComp_id_heq {a b : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') : HEq (hComp η (𝟙 (𝟙 b))) η := by
  simp [hComp_id]

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

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

Разделы

Аффилиация

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