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 } }