instStrictOfIsLocallyDiscrete — Mathlib

English

If a bicategory B is locally discrete, then B is strict.

Русский

Если би-категория B локально-дискретна, то B строго константна.

LaTeX

$$$\\forall B, [\\text{Bicategory } B], IsLocallyDiscrete B\\Rightarrow Strict B.$$$

Lean4

instance (B : Type*) [Bicategory B] [IsLocallyDiscrete B] : Strict B
    where
  id_comp f := obj_ext_of_isDiscrete (leftUnitor f).hom
  comp_id f := obj_ext_of_isDiscrete (rightUnitor f).hom
  assoc f g h := obj_ext_of_isDiscrete (associator f g h).hom

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