Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id

∀ {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₂ : B} (f : X₁ ⟶ X₂),
  F.isoMapOfCommSq ⋯ =
    CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId X₂) ≪≫
      CategoryTheory.Bicategory.rightUnitor (F.map f) ≪≫
        (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm ≪≫
          (CategoryTheory.Bicategory.whiskerRightIso (F.mapId X₁) (F.map f)).symm

Equational lemma for Pseudofunctor.isoMapOfCommSq when both horizontal maps of the square are the same and vertical maps are identities.

Defined in

Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory.StrictCategoryTheory.Bicategory