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 2) (λ { 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