eqToHomTransIso

Mathlib.CategoryTheory.Bicategory.EqToHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.eqToHomTransIso

Lean4

/-- In a bicategory, `eqToHom`s do not compose strictly,
but they do up to isomorphism. -/
def eqToHomTransIso {x y z : B} (e₁ : x = y) (e₂ : y = z) : eqToHom (e₁.trans e₂) ≅ eqToHom e₁ ≫ eqToHom e₂ :=
  e₂ ▸ e₁ ▸ (λ_ (𝟙 x)).symm

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

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

Разделы

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

Аффилиация

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