This module discusses the double-negation monad.

\begin{code}

module not-not where

open import MiniLibrary


[_] : ∀{ℓ} → Set ℓ → Set ℓ
[ X ] = (X → ∅) → ∅

hide : {X : Set} → X → [ X ]
hide x u = u x

back-to-∅ : [ ∅ ] → ∅
back-to-∅ φ = φ id

extension : {X Y : Set} → (X → [ Y ]) → [ X ] → [ Y ]
extension f φ v = φ (λ x → f x v)

\end{code}

From now on, we only use [_], hide and the above extension operator to
define everything else, and so works for any monad:

\begin{code}

[∅]-elim : {A : Set} → [ ∅ ] → A
[∅]-elim = ∅-elim ∘ back-to-∅

functor : {X Y : Set} → (X → Y) → [ X ] → [ Y ]
functor f = extension (hide ∘ f)

functor₂ : {X Y Z : Set} → (X → Y → Z) → [ X ] → [ Y ] → [ Z ]
functor₂ f xh yh = extension(λ x → functor (f x) yh) xh

Lemma[[X→Y]⇒X→[Y]] : {X : Set}{Y : X → Set} → [ ((x : X) → Y x) ] → (x : X) → [ Y x ]
Lemma[[X→Y]⇒X→[Y]] fh x = functor(λ f → f x) fh

Lemma[[X→Y]⇒[X]→[Y]] : {X Y : Set} → [ (X → Y) ] → [ X ] → [ Y ]
Lemma[[X→Y]⇒[X]→[Y]] fh = extension(Lemma[[X→Y]⇒X→[Y]] fh)

\end{code}

The double negations of identity type and related properties:

\begin{code}

[refl] : {X : Set}{x : X} → [ x ≡ x ]
[refl] = hide refl

[sym] : {X : Set}{x₀ x₁ : X} → [ x₀ ≡ x₁ ] → [ x₁ ≡ x₀ ]
[sym] = functor sym

[trans] : {X : Set}{x₀ x₁ x₂ : X} → [ x₀ ≡ x₁ ] → [ x₁ ≡ x₂ ] → [ x₀ ≡ x₂ ]
[trans] = functor₂ trans

[transport] : {X : Set}{Y : X → Set}{x x' : X} → [ x ≡ x' ] → [ Y x ] → [ Y x' ]
[transport] = functor₂ transport

[ap] : {X Y : Set} → (f : X → Y) → {x₀ x₁ : X} → [ x₀ ≡ x₁ ] → [ f x₀ ≡ f x₁ ]
[ap] f = functor (ap f)

[fun-ap] : {X Y : Set} → ∀{f g : X → Y} → [ f ≡ g ] → ∀(x : X) → [ f x ≡ g x ]
[fun-ap] eh x = functor(λ e → fun-ap e x) eh

Lemma[[≡]-Σ] : {X : Set}{P : X → Set}{x x' : X}{p : P x}{p' : P x'} →
              (e : x ≡ x') → [ transport {X} {P} e p ≡ p' ] → [ (x , p) ≡ (x' , p') ]
Lemma[[≡]-Σ] e₀ = functor (Lemma[≡-Σ] e₀)

Lemma[[≡]-∧] : {A₀ A₁ : Set}{a₀ a₀' : A₀}{a₁ a₁' : A₁} →
                [ a₀ ≡ a₀' ] → [ a₁ ≡ a₁' ] → [ ∧-intro a₀ a₁ ≡ ∧-intro a₀' a₁' ]
Lemma[[≡]-∧] = functor₂ Lemma[≡-∧]

\end{code}

The double negations of the "agree with" relation _≣[_]_, and related
properties:

\begin{code}

open import Sequence

[sym-≣[]] : {n : ℕ}{α β : ₂ℕ} → [ α ≣[ n ] β ] → [ β ≣[ n ] α ]
[sym-≣[]] = functor sym-≣[]

[trans-≣[]] : {n : ℕ}{α₀ α₁ α₂ : ₂ℕ} → [ α₀ ≣[ n ] α₁ ] → [ α₁ ≣[ n ] α₂ ] → [ α₀ ≣[ n ] α₂ ]
[trans-≣[]] = functor₂ trans-≣[]

\end{code}

If a type X is decidable, then we have ¬¬ X → X.

\begin{code}

decidable-structure : {X : Set} → decidable X → [ X ] → X
decidable-structure (in₀ x) xh = x
decidable-structure (in₁ u) xh = [∅]-elim (functor u xh)

Lemma[[≣[]]→≣[]] : {n : ℕ}{α β : ₂ℕ} → [ α ≣[ n ] β ] → α ≣[ n ] β
Lemma[[≣[]]→≣[]] {n} {α} {β} = decidable-structure (Lemma[≣[]-decidable] α β)

Lemma[[≡]→≡]-₂ : {b b' : ₂} → [ b ≡ b' ] → b ≡ b'
Lemma[[≡]→≡]-₂ {b} {b'} = decidable-structure (₂-discrete b b')

Lemma[[≡]→≡]-ℕ : {m n : ℕ} → [ m ≡ n ] → m ≡ n
Lemma[[≡]→≡]-ℕ {m} {n} = decidable-structure (ℕ-discrete m n)

open import Inequality

Lemma[[≤]→≤] : {n m : ℕ} → [ n ≤ m ] → n ≤ m
Lemma[[≤]→≤] = decidable-structure Lemma[a≤b-decidable]

\end{code}