instSmallElemForallObjCompMonCatForget₂ForgetSections

English

An instance asserts that the composite forget₂ ∘ forget MonCat has small sections, ensuring the surrounding framework applies to CommMonCat and MonCat via forgetful chains.

Русский

Экземпляр утверждает, что композит forget₂ ∘ forget MonCat имеет малые секции, обеспечивая применимость всей структуры к CommMonCat и MonCat через цепочки забываний.

LaTeX

$$$\text{Small.{u}}\; (\text{Functor.sections} ((F \downarrow forget CommMonCat) \downarrow forget MonCat))$$$

Lean4

@[to_additive]
instance : Small.{u} (Functor.sections ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) :=
  inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget CommMonCat))

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