Proof that Peirce's Law is irrefutable in intuitionistic logic.

Peirce.agda

module Peirce where

data ⊥ : Set where

⊥-elim : ∀ {A : Set} → ⊥ → A
⊥-elim ()

¬_ : Set → Set
¬_ A = A → ⊥

infixr 20 ¬_

peirce-law-irrefutable : forall {A B : Set} → ¬ ¬ (((A → B) → A) → A)
peirce-law-irrefutable {A} {B} ¬peirce-law = ¬peirce-law peirce-law
    where
    const : A → ((A → B) → A) → A
    const a ⟨a→b⟩→a = a

    a→b : A → B
    a→b a = ⊥-elim (¬peirce-law (const a))

    peirce-law : ((A → B) → A) → A
    peirce-law ⟨a→b⟩→a = ⟨a→b⟩→a a→b