Theorems · Theorem · category theory

CategoryTheory.Bicategory.leftUnitor_inv_congr

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

Defined in

Mathlib.CategoryTheory.Bicategory.EqToHom

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext

Assumes

CategoryTheory.Bicategory