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

NatD : Desc zeroL
NatD = `Σ (Fin ) 
          (λ { zero → `1 
             ; (suc zero) → `var `× `1 
             ; (suc (suc ())) })

Nat : Set 
Nat = μ NatD

ze : Nat
ze = ⟨ zero , lift tt ⟩ 

su : Nat → Nat
su n = ⟨ suc zero , n , lift tt ⟩


open import Chapter4.Desc.Lifting

module TestLifting (P : Nat → Set) where

  test-lifting-ze : [ NatD ]^ P (zero , lift tt) ≡ Lift ⊤
  test-lifting-ze = refl

  test-lifting-su : ∀{n} → [ NatD ]^ P (suc zero , n , lift tt) ≡ Σ (P n) λ _ → Lift ⊤
  test-lifting-su = refl