{-# OPTIONS --without-K --safe #-}
open import Equality
module Double-negation
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Equivalence eq hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
open import Monad eq
infix 3 ¬¬_
record ¬¬_ {a} (A : Set a) : Set a where
constructor wrap
field
run : ¬ ¬ A
open ¬¬_ public
map′ : ∀ {a b} {@0 A : Set a} {@0 B : Set b} → (A → B) → ¬¬ A → ¬¬ B
run (map′ f ¬¬a) = λ ¬b → run ¬¬a (λ a → ¬b (f a))
instance
double-negation-monad : ∀ {ℓ} → Raw-monad (λ (A : Set ℓ) → ¬¬ A)
run (Raw-monad.return double-negation-monad x) = _$ x
run (Raw-monad._>>=_ double-negation-monad x f) =
join (map′ (run ∘ f) x)
where
join : ∀ {a} {A : Set a} → ¬¬ ¬ A → ¬ A
join ¬¬¬a = λ a → run ¬¬¬a (λ ¬a → ¬a a)
private
proof-irrelevant : ∀ {a} {A : Set a} {x y : ¬¬ A} →
Extensionality a lzero → x ≡ y
proof-irrelevant ext =
cong wrap $ apply-ext ext λ _ → ⊥-propositional _ _
monad : ∀ {ℓ} →
Extensionality ℓ lzero →
Monad (λ (A : Set ℓ) → ¬¬ A)
Monad.raw-monad (monad _) = double-negation-monad
Monad.left-identity (monad ext) _ _ = proof-irrelevant ext
Monad.right-identity (monad ext) _ = proof-irrelevant ext
Monad.associativity (monad ext) _ _ _ = proof-irrelevant ext
excluded-middle : ∀ {a} {@0 A : Set a} → ¬¬ Dec A
run excluded-middle ¬[a⊎¬a] = ¬[a⊎¬a] (no λ a → ¬[a⊎¬a] (yes a))
call/cc : ∀ {a w} {@0 A : Set a} {Whatever : Set w} →
((A → Whatever) → ¬¬ A) → ¬¬ A
run (call/cc hyp) ¬a = run (hyp (λ a → ⊥-elim (¬a a))) ¬a
¬¬¬⊥ : ∀ {ℓ} → ¬ (¬¬ (⊥ {ℓ = ℓ}))
¬¬¬⊥ ¬¬⊥ = run ¬¬⊥ ⊥-elim
¬¬¬→¬ : ∀ {a} {A : Set a} → ¬¬ ¬ A → ¬ A
¬¬¬→¬ ¬¬¬a = λ a → ¬¬¬⊥ (¬¬¬a >>= λ ¬a → ⊥-elim (¬a a))
Excluded-middle : (ℓ : Level) → Set (lsuc ℓ)
Excluded-middle p = {P : Set p} → Is-proposition P → Dec P
Excluded-middle-propositional :
∀ {ℓ} →
Extensionality (lsuc ℓ) ℓ →
Is-proposition (Excluded-middle ℓ)
Excluded-middle-propositional ext =
implicit-Π-closure ext 1 λ _ →
Π-closure (lower-extensionality _ lzero ext) 1 λ P-prop →
Dec-closure-propositional (lower-extensionality _ _ ext) P-prop
Double-negation-elimination : (ℓ : Level) → Set (lsuc ℓ)
Double-negation-elimination p =
{P : Set p} → Is-proposition P → ¬¬ P → P
Double-negation-elimination-propositional :
∀ {ℓ} →
Extensionality (lsuc ℓ) ℓ →
Is-proposition (Double-negation-elimination ℓ)
Double-negation-elimination-propositional ext =
implicit-Π-closure ext 1 λ _ →
Π-closure (lower-extensionality _ lzero ext) 1 λ P-prop →
Π-closure (lower-extensionality _ lzero ext) 1 λ _ →
P-prop
Excluded-middle→Double-negation-elimination :
∀ {ℓ} → Excluded-middle ℓ → Double-negation-elimination ℓ
Excluded-middle→Double-negation-elimination em P-prop ¬¬p =
[ id , ⊥-elim ∘ run ¬¬p ] (em P-prop)
Excluded-middle≃Double-negation-elimination :
∀ {ℓ} →
Extensionality (lsuc ℓ) (lsuc ℓ) →
Excluded-middle ℓ ≃ Double-negation-elimination ℓ
Excluded-middle≃Double-negation-elimination ext =
_↔_.to (⇔↔≃ ext
(Excluded-middle-propositional
(lower-extensionality lzero _ ext))
(Double-negation-elimination-propositional
(lower-extensionality lzero _ ext)))
(record
{ to = Excluded-middle→Double-negation-elimination
; from = λ dne P-prop →
dne (Dec-closure-propositional
(lower-extensionality _ _ ext) P-prop)
excluded-middle
})