module Chapter5.Container.Examples.Vec where open import Data.Empty open import Data.Unit open import Data.Sum open import Data.Nat open import Chapter5.Container VecCont : Set → ℕ ▸ ℕ VecCont A = record { S = λ { zero → ⊤ ; (suc n) → A }; P = λ { {zero} tt → ⊥ ; {suc n} t → ⊤ } ; n = λ { {zero} {tt} () ; {suc n} tt → n } }