{-# OPTIONS --universe-polymorphism #-}
module Functor 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 Relation.Binary.PropositionalEquality
open import Function 

postulate
  -- given a type * -> *
  F : Set -> Set
  -- its corresponding relation
  [F] : ([Set] [->] [Set]) F F
  -- which is equivalent to equality when applied to equality for the argument type 
  [F]Eq->Eq : ∀ {a x y} -> [F] {a} {a} _≡_ x y -> x ≡ y
  Eq->[F]Eq : ∀ {a x y} -> x ≡ y -> [F] {a} {a} _≡_ x y

  -- two candidates for map
  map1 map2 : (a b : Set) -> (a -> b) -> F a -> F b
  -- which respect the first law
  map1-id : ∀ {a} x -> map1 a a id x ≡ x
  map2-id : ∀ {a} x -> map2 a a id x ≡ x
  
  -- and finally the parametricity result for the type of map
  free : ∀ m -> ([Π] [Set] \ [A] -> [Π] [Set] \ [B] -> ([A] [->] [B]) [->] [F] [A] [->] [F] [B]) m m


lemma : ∀ {a b : Set} -> (f : a -> b) -> ∀ x -> (map1 b b id ∘ map2 a b f) x ≡ (map1 a b f ∘ map2 a a id) x
lemma f xs = [F]Eq->Eq (free map1 (λ b a → b ≡ f a) _≡_ (λ x' → x') (free map2 _≡_ ((λ b a → b ≡ f a)) (cong f) (Eq->[F]Eq refl)))

-- we can show that the two maps give the same result for the same inputs
theorem : ∀ {a b : Set} -> (f : a -> b) -> ∀ (x : F a) -> map2 a b f x ≡ map1 a b f x
theorem f x = trans (sym (map1-id (map2 _ _ f x))) (trans (lemma f x) (cong (map1 _ _ f) (map2-id x)))