Theorems · Definition · category theory

CategoryTheory.Bicategory.whiskerLeftIso

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

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

Defined in

Mathlib.CategoryTheory.Bicategory.Basic

Cited by

48 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

CategoryTheory.Bicategory