strict — Mathlib

English

A locally discrete bicategory is strict; the associator, left and right unitors are strictly equal to their identities when computed in LocallyDiscrete.

Русский

Локально-дискретная би-категория является строгой: ассоциатор и единицы слева/справа совпадают с тождественными морфизмами.

LaTeX

$$$\\text{LocallyDiscrete B is Strict}$, i.e.,\\; id\\_comp,\\; comp\\_id,\\; assoc\\; satisfy strict equalities.$$

Lean4

/-- A locally discrete bicategory is strict. -/
instance strict : Strict (LocallyDiscrete C)
    where
  id_comp _ := Discrete.ext (Category.id_comp _)
  comp_id _ := Discrete.ext (Category.comp_id _)
  assoc _ _ _ := Discrete.ext (Category.assoc _ _ _)

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