module Chapter4.Desc.Examples.Tree 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

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

Tree : Set → Set 
Tree A = μ (TreeD A)

leaf : ∀{A} → Tree A
leaf = ⟨ zero , lift tt ⟩ 

node : ∀{A} → Tree A → A → Tree A → Tree A
node lb a rb = ⟨ suc zero , lb , a , rb , lift tt ⟩


open import Chapter4.Desc.Lifting

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

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

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