English
Given a family of truncations, there is a corresponding finite-choice constructed version into truncations.
Русский
Дана семантика усечения, существует соответствующая конструкция конечного выбора в усечениях.
LaTeX
$$$\\operatorname{Trunc.finChoice} : (\\forall i, \\operatorname{Trunc}(\\alpha i)) \\to \\operatorname{Trunc}(\\forall i, \\alpha i)$$$
Lean4
/-- Given a function that for each `i : ι` gives a term of the corresponding
truncation type, then there is corresponding term in the truncation of the product. -/
def finChoice (q : ∀ i, Trunc (α i)) : Trunc (∀ i, α i) :=
Quotient.map' id (fun _ _ _ => trivial) (Quotient.finChoice q)
