Theorems · Theorem · category theory

CategoryTheory.OplaxFunctor.mapComp_naturality_left

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (self.mapComp f' g) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g)
      (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))

Naturality of the oplax functoriality constraint, on the left.

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Cited by

2 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory