pseudofunctorLeft — Mathlib

Lean4
/-- The pseudofunctor sending `C` to `C ⋆ D`. -/
@[simps!]
def pseudofunctorLeft (D : Type u₂) [Category.{v₂} D] : Pseudofunctor Cat.{v₁, u₁} Cat.{max v₁ v₂, max u₁ u₂}
    where
  obj C := Cat.of (C ⋆ D)
  map F := mapPair F (𝟭 D)
  map₂ := (mapWhiskerRight · _)
  map₂_id {x y} f := by apply mapWhiskerRight_id
  map₂_comp η θ := by apply mapWhiskerRight_comp
  mapId D := mapPairId
  mapComp := mapCompLeft D
  map₂_whisker_left := mapWhiskerRight_whiskerLeft D
  map₂_whisker_right := mapWhiskerRight_whiskerRight D
  map₂_associator := mapWhiskerRight_associator_hom D
  map₂_left_unitor := mapWhiskerRight_leftUnitor_hom D
  map₂_right_unitor := mapWhiskerRight_rightUnitor_hom D
Похожие утверждения