Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.isoMapOfCommSq

{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₂} →
                      CategoryTheory.CommSq t l r b →
                        (CategoryTheory.CategoryStruct.comp (F.map t) (F.map r) ≅
                          CategoryTheory.CategoryStruct.comp (F.map l) (F.map b))

Given a commutative square CommSq t l r b in a strict bicategory B and a pseudofunctor from B, this is the isomorphism F.map t ≫ F.map r ≅ F.map l ≫ F.map b.

Defined in

Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory.StrictCategoryTheory.Bicategory