English
For a diagram F: J ⥤ MonCat, there is a limit cone in MonCat whose vertex is the monoidal object obtained from the Type-level limit of F after forgetting the MonCat structure, and whose legs are given by embedding the Monoid objects into MonCat via the prior projections.
Русский
Для диаграммы F: J ⥤ MonCat существует предел-конус в MonCat; вершина конуса получается из предела на уровне типов после забывания структуры MonCat, а рёбра задаются вложениями объектов моноидов в MonCat через ранее заданные проекции.
LaTeX
$$$\text{limitCone } F = \Bigl(\text{pt} := \text{MonCat.of}(\mathrm{Types.Small.limitCone}(F \downarrow \mathrm{forget MonCat})).pt,\; \pi := \{ app\ j := \text{ofHom}(\mathrm{limitπMonoidHom} F j)\,\} \Bigr)$$$
Lean4
/-- Construction of a limit cone in `MonCat`.
(Internal use only; use the limits API.)
-/
@[to_additive /-- (Internal use only; use the limits API.) -/
]
noncomputable def limitCone : Cone F :=
{ pt := MonCat.of (Types.Small.limitCone (F ⋙ forget _)).pt
π :=
{ app j := ofHom (limitπMonoidHom F j)
naturality := fun _ _ f =>
MonCat.ext fun x => CategoryTheory.congr_hom ((Types.Small.limitCone (F ⋙ forget _)).π.naturality f) x } }
