{-# OPTIONS --allow-unsolved-metas #-}

module A201602.Church where

open import Data.Product using (Σ ; _,_ ; proj₁ ; proj₂ ; _×_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)


module Rank₀ where
  List : Set  Set  Set
  List A B = (A  B  B)  B  B

  nil : ∀{A B}  List A B
  nil = λ f y₀  y₀

  cons : ∀{A B}  A  List A B  List A B
  cons x xs = λ f y₀  f x (xs f y₀)

  it : ∀{A B}  List A B  (A  B  B)  B  B
  it xs f y₀ = xs f y₀

  rec : ∀{A B C}  List A (List A C × B)  (A  List A C  B  B)  B  B
  rec xs f y₀ = proj₂ (it xs  xᵢ pᵢ  cons xᵢ (proj₁ pᵢ) , f xᵢ (proj₁ pᵢ) (proj₂ pᵢ)) (nil , y₀))

  tail : ∀{A B}  List A (List A B × List A B)  List A B
  tail xs = rec xs  xᵢ xsᵢ yᵢ  xsᵢ) nil

  data Empty : Set where
    empty : Empty

  head : ∀{A}  List A (A  Empty)  A  Empty
  head xs = it xs  xᵢ xsᵢ  inj₁ xᵢ) (inj₂ empty)


module Rank₁ where
  List : Set  Set₁
  List A = ∀{T}  (A  T  T)  T  T

  nil : ∀{A}  List A
  nil = λ f y₀  y₀

  cons : ∀{A}  A  List A  List A
  cons x xs = λ f y₀  f x (xs f y₀)

  it : ∀{A B}  List A  (A  B  B)  B  B
  it xs f y₀ = xs f y₀

--  rec : ∀{A B} → List A → (A → List A → B → B) → B → B
--  rec xs f y₀ = proj₂ (it xs (λ xᵢ pᵢ → cons xᵢ {!proj₁ pᵢ!} , f xᵢ {!proj₁ pᵢ!} (proj₂ pᵢ)) ((nil , y₀)))

  rec : ∀{A B}  List A  (A  List A  B  B)  B  B
  rec {A} {B} xs f y₀ = proj₂ (it {A} {{!List A!} × B} xs  xᵢ pᵢ  cons xᵢ {!proj₁ pᵢ!} , f xᵢ {!proj₁ pᵢ!} (proj₂ pᵢ)) ((nil , y₀)))


module WTF where
  data List (A : Set) : Set where
    nil : List A
    cons : A  List A  List A


-- module OMG where
--   data Unit : Set where
--     unit : Unit
-- ⟨x ∈ X, a ∈ A x⟩ ∈ Σ X (X → A)
--   data ListTag : Set where
--     nil  : ListTag
--     cons : ListTag

-- --  List : Set → Set
-- --  List A = Σ ListTag (λ { nil → Unit ; cons → A × List A })


-- {-module Foo where
--   data Unit : Set where
--     unit : Unit

--   data ListTag : Set where
--     nil  : ListTag
--     cons : ListTag

--   data Mu (F : Set → Set) : Set where
--     roll : F (Mu F) → Mu F

--   foo : Set → Set → ListTag → Set
--   List : Set → Set
--   foo A T nil = Unit
--   foo A T cons = A × T
--   List A = Mu (λ T → Σ ListTag (foo A T))-}


-- data mΣ {X : Set} (A : X → Set) : Set where
--      _,_ : (x₀ : X) → A x₀ → mΣ A