module Chapter5.IDesc.Examples.Bool where

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

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

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint


BoolD : func zeroL ⊤ ⊤
BoolD = func.mk λ _ → 
        `σ  (λ { zero → `1 
                ; (suc zero) → `1 
                ; (suc (suc ())) })

Bool : Set 
Bool = μ BoolD tt

true : Bool
true = ⟨ zero , lift tt ⟩

false : Bool
false = ⟨ suc zero ,  lift tt ⟩