The crisp law of excluded middle

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2024-09-23.

{-# OPTIONS --cohesion --flat-split #-}

module modal-type-theory.crisp-law-of-excluded-middle where
Imports 
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.decidable-propositions
open import foundation-core.propositions

Idea

The crisp law of excluded middle asserts that any crisp proposition P is decidable.

Definition

Crisp-LEM : (@♭ l : Level) → UU (lsuc l)
Crisp-LEM l = (@♭ P : Prop l) → is-decidable (type-Prop P)

Properties

Given crisp LEM, we obtain a map from crisp propositions to decidable propositions

decidable-prop-Crisp-Prop :
  {@♭ l : Level} → Crisp-LEM l → @♭ Prop l → Decidable-Prop l
pr1 (decidable-prop-Crisp-Prop lem P) = type-Prop P
pr1 (pr2 (decidable-prop-Crisp-Prop lem P)) = is-prop-type-Prop P
pr2 (pr2 (decidable-prop-Crisp-Prop lem P)) = lem P

See also

References

[Shu18]
Michael Shulman. Brouwer's fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856–941, 06 2018. arXiv:1509.07584, doi:10.1017/S0960129517000147.

Recent changes