module EmptyF where

open import Level

-- Setting up the parametricity relations

Π : {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

[Set] : [Set (suc zero) ] 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 _[->]_

open import Data.List
open import Relation.Binary.PropositionalEquality
open import Data.Empty

data [List] {A1 A2 : Set}([A] : [Set] A1 A2) : [Set] (List A1) (List A2) where
  [] : [List] [A] [] []
  _[∷]_ : ([A] [->] [List] [A] [->] [List] [A]) _∷_ _∷_

postulate
  para-f : ∀ f -> ([Π] [Set] \ [T] -> [List] [T] [->] [List] [T]) f f

theorem : (f : ( (T : Set) → List T → List T  ) ) → ( A : Set) → f A [] ≡ []
theorem f A with f A [] | para-f f {A} {A} (\ _ _ -> ⊥) []
theorem f A | .[] | [] = refl
theorem f A | .(a1 ∷ a2) | _[∷]_ {a1} () {a2} aR'