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 λ _ → `σ 2 (λ { 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 ⟩