The crisp law of excluded middle
Content created by Fredrik Bakke.
Created on 2023-11-24.
Last modified on 2023-11-24.
{-# 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.negation 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
Recent changes
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).