isoMapOfCommSq

Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pseudofunctor.isoMapOfCommSq

Lean4

/-- Given a commutative square `CommSq t l r b` in a strict bicategory `B` and
a pseudofunctor from `B`, this is the natural isomorphism
`F.map t ≫ F.map r ≅ F.map l ≫ F.map b`. -/
def isoMapOfCommSq : F.map t ≫ F.map r ≅ F.map l ≫ F.map b :=
  (F.mapComp t r).symm ≪≫ F.mapComp' _ _ _ (by rw [sq.w])

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

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

Разделы

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

Аффилиация

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