Homotopy Type Theory
limited principle of omniscience

The limited principle of omniscience (LPO), the weak limited principle of omniscience (WLPO), and the lesser limited principle of omniscience (LLPO) are classicality axioms that are weaker than excluded middle?. For now, see the nlab for their statements.

They can be translated into HoTT in two ways, by interpreting “or” as truncated (“merely or”) or untruncated (“purely or”). The relationships are: