📥 Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.ComputationalContent.DoubleNegation (⊥ : Set) where

Sarcastic interpretation of classical logic

Explain.

open import Padova2025.ProvingBasics.Connectives.Disjunction

infix 3 ¬_
¬_ : Set → Set  -- enter `¬` as `\neg`
¬ P = (P → ⊥)

return : {A : Set} → A → ¬ ¬ A
return = {!!}

⊥-elim : {A : Set} → ⊥ → ¬ ¬ A
⊥-elim = {!!}

escape : ¬ ¬ ⊥ → ⊥
escape = {!!}

oracle : {A : Set} → ¬ ¬ (A ⊎ ¬ A)
oracle = {!!}

infixl 1 _>>=_ _⟫=_

_>>=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
_>>=_ = {!!}

_⟫=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
_⟫=_ = _>>=_