Homotopy Type Theory limited principle of omniscience > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

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:

Definition

The truncated limited principle of omniscience for a type AA states that for every boolean predicate on AA, either it is the constant function into 00 or the fiber of the boolean predicate at 11 is inhabited:

P:A𝟚[[fiber(P,1)]+ a:AP(a)=0]\prod_{P:A \to \mathbb{2}} \left[\left[fiber(P, 1)\right] + \prod_{a:A} P(a) = 0\right]

Properties

See also

Revision on June 14, 2022 at 02:28:04 by Anonymous?. See the history of this page for a list of all contributions to it.