Theorems · Definition · category theory

CategoryTheory.Bicategory.associatorNatIsoLeftCat

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a : B) →
      {b c d : B} →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.postcomposingCat a b c).obj g)
                ((CategoryTheory.Bicategory.postcomposingCat a c d).obj h) ≅
              (CategoryTheory.Bicategory.postcomposingCat a b d).obj (CategoryTheory.CategoryStruct.comp g h)

Left component of the associator as a 2-isomorphism in Cat.

Defined in

Mathlib.CategoryTheory.Bicategory.Yoneda

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory