final_fromPUnit_of_isTerminal — Mathlib

English

If c is terminal, the functor from the one-point category to c is final.

Русский

Если c является терминальным объектом, то функтор fromPUnit(c): 1 → C финален.

LaTeX

$$$\operatorname{IsTerminal}(c) \Rightarrow \operatorname{Final}(\operatorname{fromPUnit}(c))$$$

Lean4

theorem final_fromPUnit_of_isTerminal (hc : Limits.IsTerminal c) : (fromPUnit c).Final where
  out
    c' := by
    letI : Inhabited (StructuredArrow c' (fromPUnit c)) := ⟨.mk (Y := default) (hc.from c')⟩
    letI : Subsingleton (StructuredArrow c' (fromPUnit c)) :=
      ⟨fun i j ↦ StructuredArrow.obj_ext _ _ (by cat_disch) (hc.hom_ext _ _)⟩
    infer_instance

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