Theorems · Theorem · category theory

CategoryTheory.StrictPseudofunctor.map_comp

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

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Cited by

3 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory