Can we regard the following function as proof? Can we read it as
conversion of statement ((P→⊥)→⊥) to ((⊥→⊥)→⊥) with last ⊥ encoded by
nontermination?
{-# OPTIONS --no-termination-check #-}
module DoubleNegation where
data ⊥ : Set where
⊥⊥→⊥ : {P : Set}
→ ((P → ⊥) → ⊥)
→ (P → ⊥)
⊥⊥→⊥ {P} double = h
where
h : P → ⊥
h P = double h