English
An auxiliary construction provides a limit cone for the diagram F after applying the forgetful mapping to MonCat; this auxiliary limit accelerates typechecking.
Русский
Вспомогательное построение даёт предел-конус диаграммы F после применения забывающего отображения в MonCat; этот вспомогательный предел ускоряет типизацию.
LaTeX
$$$\text{forget}_2\, SemiRingCat\, MonCat\;:\; \text{IsLimit}\big((\operatorname{forget}_2 SemiRingCat MonCat)\!\.mapCone(\operatorname{limitCone} F)\big)$$$
Lean4
/-- An auxiliary declaration to speed up typechecking.
-/
def forget₂MonPreservesLimitsAux : IsLimit ((forget₂ SemiRingCat MonCat).mapCone (limitCone F)) :=
by
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ MonCat) ⋙ forget MonCat)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget SemiRingCat))
apply MonCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ SemiRingCat MonCat.{u})
