StructuralOfExpr_bicategoricalComp

Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Bicategory.StructuralOfExpr_bicategoricalComp

Lean4

theorem StructuralOfExpr_bicategoricalComp {f g h i : a ⟶ b} [BicategoricalCoherence g h] (η : f ⟶ g) (η' : f ≅ g)
    (ih_η : η'.hom = η) (θ : h ⟶ i) (θ' : h ≅ i) (ih_θ : θ'.hom = θ) : (bicategoricalIsoComp η' θ').hom = η ⊗≫ θ := by
  simp [ih_η, ih_θ, bicategoricalIsoComp, bicategoricalComp]

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

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

Разделы

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

Аффилиация

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