module Chapter9.FunOrnament.Examples.Lookup where

open import Data.Unit

open import Chapter2.Logic

open import Chapter5.IDesc.Examples.Nat

open import Chapter8.Ornament
open import Chapter8.Ornament.Identity
open import Chapter8.Ornament.Examples.List
open import Chapter8.Ornament.Examples.Maybe

open import Chapter9.Functions.Examples.Le

open import Chapter9.FunOrnament

typeLookup : (A : Set) → FunctionOrn type<
typeLookup A = μ⁺ idO NatD [ inv tt ]→ 
               μ⁺ ListO A [ inv tt ]→ 
               μ⁺ MaybeO A [ inv tt ]× `⊤