English
The limit cone constructed in MonCat is actually a limit cone for the diagram F; i.e., it satisfies the universal property of a limit in MonCat.
Русский
Предел-конус, построенный в MonCat, действительно является пределом для диаграммы F; то есть он удовлетворяет универсальной свойству предела в MonCat.
LaTeX
$$$\mathrm{IsLimit}(\text{limitCone } F)$$$
Lean4
/-- Witness that the limit cone in `MonCat` is a limit cone.
(Internal use only; use the limits API.)
-/
@[to_additive /-- (Internal use only; use the limits API.) -/
]
noncomputable def limitConeIsLimit : IsLimit (limitCone F) :=
by
refine
IsLimit.ofFaithful (forget MonCat) (Types.Small.limitConeIsLimit.{v, u} _)
(fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_ }) (fun s => rfl)
· simp only [Functor.mapCone_π_app, forget_map, map_one]
rfl
· intro x y
simp only [EquivLike.coe_apply, Functor.mapCone_π_app, forget_map, map_mul]
rw [← equivShrink_mul]
rfl
