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 ⟩