# The crisp law of excluded middle

Content created by Fredrik Bakke.

Created 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