Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq

∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ Y₁ Y₂ : B} {t : X₁ ⟶ Y₁}
  {l : X₁ ⟶ X₂} {r : Y₁ ⟶ Y₂} {b : X₂ ⟶ Y₂} (sq : CategoryTheory.CommSq t l r b) (φ : X₁ ⟶ Y₂)
  (hφ : CategoryTheory.CategoryStruct.comp t r = φ),
  F.isoMapOfCommSq sq = (F.mapComp' t r φ ⋯).symm ≪≫ F.mapComp' l b φ ⋯

Defined in

Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Cited by

2 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory.StrictCategoryTheory.Bicategory