Theorems · Definition · category theory

CategoryTheory.Bicategory.leftZigzag

{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g) →
            (CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b) →
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ⟶
                CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))

The 2-morphism defined by the following pasting diagram: `` a －－－－－－ ▸ a ＼ η ◥ ＼ f ＼ g ／ ＼ f ◢ ／ ε ◢ b －－－－－－ ▸ b ``

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory