Theorems · Definition · category theory

CategoryTheory.Bicategory.whiskerRightIso

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

The right whiskering of a 2-isomorphism is a 2-isomorphism.

Defined in

Mathlib.CategoryTheory.Bicategory.Basic

Cited by

50 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

CategoryTheory.Bicategory