mapId'_eq_mapId

Mathlib.CategoryTheory.Bicategory.Functor.Lax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.LaxFunctor.mapId'_eq_mapId

English

For a morphism η : f ⟶ g, the inverse map satisfies F.map₂ inv η ≡ inv (F.map₂ η).

Русский

Для морфизма η: f ⟶ g сохраняется равенство F.map₂ inv η = inv (F.map₂ η).

LaTeX

$$$F.map₂ (inv \eta) = inv (F.map₂ \eta)$$$

Lean4

theorem mapId'_eq_mapId (b : B) : F.mapId' (𝟙 b) rfl = F.mapId b := by simp [mapId']

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

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

Разделы

Аффилиация

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