module parametricity2 where

open import Level

--------------------------------------
-- Parametricity theorem generator by
--  Jean-Philippe Bernardy
-- http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.LightweightFreeTheorems
--------------------------------------

Π : {l m : Level} (A : Set l) (B : A → Set m) → Set (l ⊔ m)
Π A B = (a : A) → B a


[Set_] : ∀ l → Set l → Set l → Set (suc l)
[Set l ] A1 A2 = A1 → A2 → Set l

[Set2] = [Set suc (suc zero) ]

[Set1] : [Set2] Set1 Set1
[Set1] = [Set suc zero ]

[Set] : [Set1] Set Set
[Set] = [Set zero ]


[Π] : {l m : Level} {A1 A2 : Set l} {B1 : A1 → Set m} {B2 : A2 → Set m} →
            ([A] : [Set l ] A1 A2) →
            ([B] : ∀ {a1 a2} → (aR : [A] a1 a2) → [Set m ] (B1 a1) (B2 a2) ) →
            [Set (l ⊔ m) ] (Π A1 B1) (Π A2 B2)
([Π] [A] [B]) f1 f2 = ∀ {a1 a2} → (aR : [A] a1 a2) → [B] {a1} {a2} aR (f1 a1) (f2 a2)


_[→]_ : {l m : Level} {A1 A2 : Set l} {B1 B2 : Set m} →
            ([A] : [Set l ] A1 A2) →
            ([B] : [Set m ] B1 B2) →
            [Set (l ⊔ m) ] (A1 → B1) (A2 → B2)
[A] [→] [B] = [Π] [A] (\_ → [B])

infixr 0 _[→]_


module Lem where

--------------------------------------
-- Definitions
--------------------------------------


data ⊥ : Set where

[⊥] : [Set] ⊥ ⊥
[⊥] _ _ = ⊥

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

[¬]_ : ∀ {A₁ A₂} ([A] : [Set] A₁ A₂) → [Set] (¬ A₁) (¬ A₂)
[¬] [A] = [A] [→] [⊥]

data Dec (A : Set) : Set where
  yes : A → Dec A
  no : ¬ A → Dec A

data [Dec] {A1 A2 : Set} ([A] : [Set] A1 A2) : [Set] (Dec A1) (Dec A2) where
  yes : ([A] [→] [Dec] [A]) yes yes
  no : ([¬] [A] [→] [Dec] [A]) no no

LEM : Set1
LEM = Π Set Dec

[LEM] : [Set1] LEM LEM
[LEM] = [Π] [Set] [Dec]

Free-Theorem-LEM = (l : LEM) → [LEM] l l

--------------------------------------
-- Proof
--------------------------------------

record ⊤ : Set where

data IsNo {A : Set} : Dec A → Set where
  no : ∀ {x} → IsNo (no x)

data IsYes {A : Set} : Dec A → Set where
  yes : ∀ {x} → IsYes (yes x)

contra : ∀ {A B : Set} {a : Dec A} {b : Dec B} {r} → IsNo a → IsYes b → [Dec] r a b → ⊥
contra no yes ()

no⊥ : ∀ (l : LEM) → IsNo (l ⊥)
no⊥ l with l ⊥
no⊥ l | yes ()
no⊥ l | no y = no

yes⊤ : ∀ (l : LEM) → IsYes (l ⊤)
yes⊤ l with l ⊤
yes⊤ l | yes _ = yes
yes⊤ l | no n with n (record {})
... | ()

¬lem : Free-Theorem-LEM → LEM → ⊥
¬lem theorem lem = contra (no⊥ lem) (yes⊤ lem) (theorem lem {⊥} {⊤} (λ _ _ → ⊤))