Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adjunction.comp_right_triangle_aux

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b}
  (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂),
  CategoryTheory.Bicategory.rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp g₂ g₁)).hom
      (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp g₂ g₁)).inv

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory