empty_of_initial_of_preserves — Mathlib

English

If forgetful preserves initial objects, then initial X implies ToType X is empty.

Русский

Если забывающий функтор сохраняет начальные объекты, то начальный X приводит к пустому ToType X.

LaTeX

$$$ \\text{empty_of_initial_of_preserves } $$$

Lean4

/-- If `forget C` preserves initials and `X` is initial, then `ToType X` is empty. -/
theorem empty_of_initial_of_preserves [PreservesColimit (Functor.empty.{0} C) (forget C)] (X : C)
    (h : Nonempty (IsInitial X)) : IsEmpty (ToType X) :=
  by
  rw [← Types.initial_iff_empty]
  exact Nonempty.map (IsInitial.isInitialObj (forget C) _) h

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