module Chapter4.Desc.Examples.List where

open import Level
  renaming ( zero to zeroL
           ; suc to sucL )

open import Data.Unit
open import Data.Product
open import Data.Fin hiding (lift)

open import Relation.Binary.PropositionalEquality

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint

ListD : Set → Desc zeroL
ListD A = `Σ (Fin ) 
             (λ { zero → `1 
                ; (suc zero) → `Σ A λ _ → `var `× `1 
                ; (suc (suc ())) })

List : Set → Set 
List A = μ (ListD A)

nil : ∀{A} → List A
nil = ⟨ zero , lift tt ⟩ 

cons : ∀{A} → A → List A → List A
cons a xs = ⟨ suc zero , a , xs , lift tt ⟩


open import Chapter4.Desc.Lifting

module TestLifting {A : Set}(P : List A → Set) where

  test-lifting-nil : [ ListD A ]^ P (zero , lift tt) ≡ Lift ⊤
  test-lifting-nil = refl

  test-lifting-cons : ∀{a xs} → [ ListD A ]^ P (suc zero , a , xs , lift tt) ≡ Σ (P xs) λ _ → Lift ⊤
  test-lifting-cons = refl