mkOfTerminalΩ₀ — Mathlib

Lean4
/-- More explicit constructor in case `Ω₀` is already known to be a terminal object. -/
@[simps]
def mkOfTerminalΩ₀ (Ω₀ : C) (t : IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : ∀ {U X : C} (m : U ⟶ X) [Mono m], X ⟶ Ω)
    (isPullback : ∀ {U X : C} (m : U ⟶ X) [Mono m], IsPullback m (t.from U) (χ m) truth)
    (uniq : ∀ {U X : C} (m : U ⟶ X) [Mono m] (χ' : X ⟶ Ω) (_ : IsPullback m (t.from U) χ' truth), χ' = χ m) :
    Classifier C where
  Ω₀ := Ω₀
  Ω := Ω
  truth := truth
  mono_truth := t.mono_from _
  χ₀ := t.from
  χ m _ := χ m
  isPullback m _ := isPullback m
  uniq m _ χ₀' χ' hχ' := uniq m χ' ((t.hom_ext χ₀' (t.from _)) ▸ hχ')
Похожие утверждения