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 ⟩