module Chapter8.Reornament.Examples.Maybe
         (A : Set) 
       where

open import Level

open import Data.Unit
open import Data.Product

open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Examples.Bool

open import Chapter8.Ornament
open import Chapter8.Ornament.Examples.Maybe

open import Chapter8.Reornament (MaybeO A)

iMaybe : Bool  Set
iMaybe b = μ reornD (tt , b)

inothing : iMaybe false
inothing =  lift tt , lift tt  

ijust : A  iMaybe true
ijust a =  (a , lift tt) , lift tt