pseudofunctorRight — Mathlib

Lean4
/-- The pseudofunctor sending `D` to `C ⋆ D`. -/
@[simps!]
def pseudofunctorRight (C : Type u₁) [Category.{v₁} C] : Pseudofunctor Cat.{v₂, u₂} Cat.{max v₁ v₂, max u₁ u₂}
    where
  obj D := Cat.of (C ⋆ D)
  map F := mapPair (𝟭 C) F
  map₂ := mapWhiskerLeft _
  map₂_id {x y} f := by apply mapWhiskerLeft_id
  map₂_comp η θ := by apply mapWhiskerLeft_comp
  mapId D := mapPairId
  mapComp := mapCompRight C
  map₂_whisker_left := mapWhiskerLeft_whiskerLeft C
  map₂_whisker_right := mapWhiskerLeft_whiskerRight C
  map₂_associator := mapWhiskerLeft_associator_hom C
  map₂_left_unitor := mapWhiskerLeft_leftUnitor_hom C
  map₂_right_unitor := mapWhiskerLeft_rightUnitor_hom C
Похожие утверждения