-- Please ignore the prelude
-- START of the prelude

postulate
  magic : ∀ {i} {X : Set i} → X

Type = Set₀

data _+_ (A : Type) (B : Type) : Type where
  inl : A → A + B
  inr : B → A + B
infixr 4 _+_

record _×_ (A : Type) (B : Type) : Type where
  constructor _,_
  field
    fst : A
    snd : B
open _×_ public
infixr 4 _,_

data ⊥ : Type where

record ⊤ : Set where
  constructor tt

-- END of the prelude

¬_ : Type → Type
¬ A = A → ⊥

modus-ponens : ∀ {A B : Type} → (A → B) → A → B
modus-ponens f x = f x

explosion : ∀ {A : Type} → ⊥ → A
explosion ()

case : ∀ {A B C : Type} → (A → C) → (B → C) → (A + B → C)
case f g (inl x) = f x
case f g (inr y) = g y

contraposition : ∀ {A B : Type} → (A → B) → (¬ B → ¬ A)
contraposition f ¬b a = ¬b (f a)

-- Double negation translation
--
-- Gilvenko did it for propositional logic.
-- Gödel and Gentzen, and Kuroda (two variants) did it for first-order logic.

⟦_⟧ : Type → Type
⟦ A ⟧ = ¬ ¬ A

⟦⟧-embed : ∀ {A : Type} → A → ⟦ A ⟧
⟦⟧-embed a ¬a = ¬a a

⟦⟧-embed' : ∀ {A : Type} → A → ((A → ⊥) → ⊥)
⟦⟧-embed' a ¬a = ¬a a

⟦⟧-¬ : ∀ {A : Type} → ⟦ ¬ A ⟧ → ¬ A
⟦⟧-¬ ¬¬¬a a = ¬¬¬a (λ ¬a → ¬a a)

⟦⟧-¬' : ∀ {A : Type} → ¬ ⟦ A ⟧ → ¬ A
⟦⟧-¬' = contraposition ⟦⟧-embed

⟦⟧-map : ∀ {A B : Type} → (A → B) → (⟦ A ⟧ → ⟦ B ⟧)
⟦⟧-map f ¬¬a ¬b = ¬¬a (λ a → ¬b (f a))

⟦⟧-map2 : ∀ {A B C : Type} → (A → B → C) → (⟦ A ⟧ → ⟦ B ⟧ → ⟦ C ⟧)
⟦⟧-map2 f ¬¬a ¬¬b ¬c = ¬¬a (λ a → ¬¬b (λ b → ¬c (f a b)))

-- p : A × B
-- fst p : A
-- snd p : B

-- Unicode trivia:
--
-- "‚" <-- This is U+201A, not the English comma "," U+002C.
-- "꞉" <-- This is U+A789, not the English colon ":" U+003A.
--
-- Now you know what to do on April 1st this year. *wink*

⟦⟧-pair : ∀ {A B : Type} → ⟦ A ⟧ → ⟦ B ⟧ → ⟦ A × B ⟧
⟦⟧-pair = ⟦⟧-map2 _,_

⟦⟧-fst : ∀ {A B : Type} → ⟦ A × B ⟧ → ⟦ A ⟧
⟦⟧-fst = ⟦⟧-map fst

⟦⟧-snd : ∀ {A B : Type} → ⟦ A × B ⟧ → ⟦ B ⟧
⟦⟧-snd = ⟦⟧-map snd

⟦⟧-inl : ∀ {A B : Type} → ⟦ A ⟧ → ⟦ A + B ⟧
⟦⟧-inl = ⟦⟧-map inl

⟦⟧-inr : ∀ {A B : Type} → ⟦ B ⟧ → ⟦ A + B ⟧
⟦⟧-inr = ⟦⟧-map inr

⟦⟧-case : ∀ {A B C : Type} → ⟦ (A → C) ⟧ → ⟦ (B → C) ⟧ → ⟦ (A + B → C) ⟧
⟦⟧-case = ⟦⟧-map2 case

-- Exercise: we will discuss this on 1/30

⟦⟧-LEM : ∀ {A : Type} → ⟦ A + ¬ A ⟧
⟦⟧-LEM ¬lem = ¬lem (inr (λ a → ¬lem (inl a)))