Chuangjie Xu 2013 (updated in February 2015)

This module discusses the double-negation monad.

\begin{code}

{-# OPTIONS --without-K #-}

module UsingNotNotFunext.NotNot where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber hiding (_+_)
open import Preliminaries.Boolean


infixl  ¬¬_

¬¬_ : ∀{ℓ} → Set ℓ → Set ℓ
¬¬_ X = ¬ (¬ X)

Theorem[¬¬-final] :

  ∀(T : Set → Set) → (∀{A B} → (A → B) → T A → T B) → (T ∅ → ∅) →

  ∀{A} → T A → ¬¬ A

Theorem[¬¬-final] T fT eT ta na = eT (fT na ta)


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)

¬¬∅-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)

decidable-structure : {X : Set} → decidable X → ¬¬ X → X
decidable-structure (inl x) xh = x
decidable-structure (inr u) xh = ¬¬∅-elim (functor u xh)

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

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

\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 _⁻¹

¬¬trans : {X : Set}{x₀ x₁ x₂ : X} → ¬¬ x₀ ≡ x₁ → ¬¬ x₁ ≡ x₂ → ¬¬ x₀ ≡ x₂
¬¬trans = functor₂ _·_

¬¬transport : {X : Set}{x x' : X}(Y : X → Set)
            → ¬¬ x ≡ x' → ¬¬ Y x → ¬¬ Y x'
¬¬transport Y = functor₂ (transport Y)

¬¬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

¬¬pair⁼ : {X : Set}{Y : X → Set}{x x' : X}{y : Y x}{y' : Y x'}
        → (p : x ≡ x') → ¬¬ transport Y p y ≡ y' → ¬¬ (x , y) ≡ (x' , y')
¬¬pair⁼ p = functor (pair⁼ p)

¬¬pairˣ⁼ : {X Y : Set} {x x' : X} {y y' : Y}
         → ¬¬ x ≡ x' → ¬¬ y ≡ y' → ¬¬ (x , y) ≡ (x' , y')
¬¬pairˣ⁼ = functor₂ pairˣ⁼

\end{code}