Theorems · Definition · category theory

CategoryTheory.Bicategory.rightUnitor

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

The right unitor: f ≫ 𝟙 b ≅ f

Defined in

Mathlib.CategoryTheory.Bicategory.Basic

Cited by

308 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 12 definitions · uses no axioms

Assumes

CategoryTheory.Bicategory