Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathcal {E}(i)\) is closed under propositional truncation.
Proof
This is because propositional truncation is constructed by countable coproducts, finite limits, and finite colimits by the join construction [Rijke--2017-0000].