eqToHom_hComp_eqToHom

Mathlib.CategoryTheory.Bicategory.CatEnriched

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

Lean4

@[simp]
theorem eqToHom_hComp_eqToHom {a b c : CatEnrichedOrdinary C} {f f' : a ⟶ b} (α : f = f') {g g' : b ⟶ c} (β : g = g') :
    hComp (eqToHom α) (eqToHom β) = eqToHom (α ▸ β ▸ rfl) := by cases α; cases β; simp

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

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

Разделы

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

Аффилиация

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