module Fold where
open import Relation.Binary.PropositionalEquality

postulate
  F : Set -> Set
  fmap : ∀ {a b} -> (a -> b) -> F a -> F b
  fmap-id : ∀ {a} -> {x : F a} -> fmap (\ (x : a) -> x) x ≡ x
  ext : ∀ {l1 l2} {a : Set l1}{b : a -> Set l2} -> {f g : (x : a) -> b x} -> (∀ x -> f x ≡ g x) -> f ≡ g

Alg : (Set -> Set) -> Set -> Set
Alg f a = f a -> a

Cont : Set -> Set -> Set
Cont r a = (a -> r) -> r

iso : ∀ {c} -> Alg F c -> (∀ a -> F a -> Cont c a)
iso a _ u = \ g -> a (fmap g u)

iso' : ∀ {c} -> (∀ a -> F a -> Cont c a) -> Alg F c
iso' sigma = λ u → sigma _ u (λ x → x)

prop1 : ∀ {c} -> (σ : Alg F c) -> iso' (iso σ) ≡ σ
prop1 {c} σ = ext (λ x → cong σ fmap-id)

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 _[->]_

postulate
  [F] : ([Set] [->] [Set]) F F
  [F]-refl : ∀ {a : Set} {x : F a} -> [F] _≡_ x x
  [σ] : ∀ {c}  -> (σ : (∀ a -> F a -> Cont c a)) -> ([Π] [Set] \ [a] -> [F] [a] [->] ([a] [->] _≡_) [->] _≡_) σ σ
  [fmap] : ([Π] [Set] \ [a] -> [Π] [Set] \ [b] -> ([a] [->] [b]) [->] [F] [a] [->] [F] [b]) (\ _ _ -> fmap) (\ _ _ -> fmap)


prop2 : ∀ {c} -> (σ : (∀ a -> F a -> Cont c a)) -> iso (iso' σ) ≡ σ
prop2 {c} σ = ext
                (λ a →
                   ext
                   (λ Fa →
                      ext
                      (λ g →
                         [σ] σ (λ c' a' → c' ≡ g a')
                         (subst ([F] (λ c' a' → c' ≡ g a') (fmap g Fa)) fmap-id
                          ([fmap] _≡_ (λ c' a' → c' ≡ g a') (cong g) [F]-refl))
                         (λ c≡ga → c≡ga))))