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 [[nlab:principle of omniscience|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: * Truncated LPO and untruncated LPO are equivalent; see Exercise 3.19 in [[the HoTT book]]. (due to Martin Escardo) * Similarly, truncated WLPO and untruncated WLPO are equivalent. * Untruncated LLPO is equivalent to WLPO (also due to Martin Escardo). * In <http://www1.maths.leeds.ac.uk/~rathjen/Lifschitz.pdf> is a model by Michael Rathjen that separates WLPO from LLPO.