module parametricity where

import Level
open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning

-- The parametricity definition was stolen from Daniel Peebles.

-- Legend has it that parametricity is just dinaturality
module Parametricity {a} {F G : Set a → Set a → Set a}
                         (mapF : ∀ {A B C D} → (A → B) → (C → D) → F B C → F A D)
                         (mapG : ∀ {A B C D} → (A → B) → (C → D) → G B C → G A D)
                         where
  postulate
    -- Agda doesn't know that its own polymorphic functions are dinatural, so we must teach it about itself
    dinatural : ∀ (f : ∀ {A} → F A A → G A A) {A B : Set a} (g : A → B) → ∀ x → mapG id g (f (mapF g id x)) ≡ mapG g id (f (mapF id g x))


open import Relation.Nullary

open import Data.Unit
open import Data.Empty
open import Data.Sum

data IsInj₁ {A B : Set} : A ⊎ B → Set where
  inj₁ : ∀ {x : A} → IsInj₁ (inj₁ x)

data IsInj₂ {A B : Set} : A ⊎ B → Set where
  inj₂ : ∀ {x : B} → IsInj₂ (inj₂ x)


LEM = ∀ {A : Set} → Dec A
LEM' = ∀ {A : Set} → ⊤ → A ⊎ ¬ A

map⊎¬ : ∀ {A B C D : Set} → (A → B) → (C → D) → C ⊎ ¬ B → D ⊎ ¬ A
map⊎¬ ab cd (inj₁ c) = inj₁ (cd c)
map⊎¬ ab cd (inj₂ b) = inj₂ (λ a → b (ab a))

map⊤ : ∀ {A B C D : Set} → (A → B) → (C → D) → ⊤ → ⊤
map⊤ _ _ = id

contra : ∀ {A B : Set} (g : A → B) → ∀ {l r} → IsInj₂ l → IsInj₁ r → ¬ (map⊎¬ id g l ≡ map⊎¬ g id r)
contra g inj₂ inj₁ ()

lem-⊥ : ∀ (lem : LEM') → IsInj₂ (lem {⊥} tt)
lem-⊥ lem with lem {⊥} tt
lem-⊥ lem | inj₁ ()
lem-⊥ lem | inj₂ y = inj₂

lem-⊤ : ∀ (lem : LEM') → IsInj₁ (lem {⊤} tt)
lem-⊤ lem with lem {⊤} tt
lem-⊤ lem | inj₁ x = inj₁
lem-⊤ lem | inj₂ y = ⊥-elim (y tt)

¬lem' : ¬ LEM'
¬lem' lem =  contra ⊥-elim (lem-⊥ lem) (lem-⊤ lem) (dinatural lem {⊥} {⊤} (⊥-elim) tt)  where
  open Parametricity {_} {λ _ _ → ⊤} {λ A B → B ⊎ ¬ A} map⊤ map⊎¬

lem⇒lem' : LEM → LEM'
lem⇒lem' lem {A} tt with lem {A}
lem⇒lem' lem tt | yes p = inj₁ p
lem⇒lem' lem tt | no ¬p = inj₂ ¬p

¬lem : ¬ LEM
¬lem lem = ¬lem' (lem⇒lem' lem)