The propositional truncation of a W-type is a proposition

Proved

LeanTT2.subsingleton_realizable

by Lucas · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

propositionaltruncationsubsingletonstypetheoryw-types

For every extended fragment, context, and branching presentation A, B with A a type and B typed at the function type from A into the universe: the propositional truncation of the W-type of the presentation is a type, and it is a proposition. The truncation is the nonempty operation of thesis section 5.1, the tool that constructs small eliminators in the reduction of chapter 5.

Preamble

import Mathlib
import Definitions.Def_LeanTT2_frag
import Definitions.Def_LeanTT2_spec
import Definitions.Def_LeanTT2_counter

Formal statement

universe u

/-!
# Subsingleton truncations of W-types

The propositional truncation of a W-type is a type and a proposition.
The truncation former is the nonempty operation of thesis section 5.1
(page 27), which produces a proposition from any type; it is the tool
used to construct small eliminators, and the subsingleton clause of the
realization correctness predicate is its counterpart (thesis section
5.3, page 31).
-/

namespace LeanTT2

/-- For every extended fragment, context, and branching presentation
`A`, `B` with `A` a type and `B` typed at `A → Univ`: the propositional
truncation of the W-type `wT A B` is a type, and it is a proposition. -/
theorem subsingleton_realizable (F : Frag.{u}) (Γ : F.Ctx) (A B : F.E)
    (hA : F.isType Γ A) (hB : F.ty Γ B (F.piT A F.Univ)) :
    F.isType Γ (F.truncT (F.wT A B)) ∧
    F.isProp Γ (F.truncT (F.wT A B)) := by sorry

end LeanTT2

Source

M. Carneiro, The Type Theory of Lean, 2019, sections 5.1 and 5.3 (pp. 27, 31).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: in any extended fragment, the propositional truncation of a W-type of a branching presentation is both a type and a proposition in its context.

View graph