Lean4
/-- `Trunc α` is the quotient of `α` by the always-true relation. This
is related to the propositional truncation in HoTT, and is similar
in effect to `Nonempty α`, but unlike `Nonempty α`, `Trunc α` is data,
so the VM representation is the same as `α`, and so this can be used to
maintain computability. -/
def Trunc.{u} (α : Sort u) : Sort u :=
@Quotient α trueSetoid