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 ]× `⊤