Theorems · Theorem · category theory

CategoryTheory.Bicategory.rightUnitor_inv_congr

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f'),
  (CategoryTheory.Bicategory.rightUnitor f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f').inv
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.id y)))

Defined in

Mathlib.CategoryTheory.Bicategory.EqToHom

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext

Assumes

CategoryTheory.Bicategory