toOplaxFunctor' — Mathlib

English

The map on the identity 2-morphism maps to the identity: F.map₂ (id f) = id (F.map f).

Русский

Отображение на тождественный 2-морфизм даёт тождественный морфизм: F.map₂ (id f) = id (F.map f).

LaTeX

$$$F.map₂ (id f) = id (F.map f)$$$

Lean4

/-- If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categories) `I ⥤ B` can
be promoted to an oplax functor from `LocallyDiscrete I` to `B`.
-/
@[simps! obj map mapId mapComp]
abbrev toOplaxFunctor' : OplaxFunctor (LocallyDiscrete I) B :=
  F.toPseudoFunctor'.toOplax

Похожие утверждения