module Chapter5.Container.Examples.List where

open import Data.Empty
open import Data.Unit
open import Data.Sum

open import Chapter5.Container

ListCont : Set → ⊤ ▸ ⊤
ListCont A = record { 
            S = λ tt → ⊤ ⊎ A; 
            P = λ { (inj₁ tt) → ⊥ 
                  ; (inj₂ a) → ⊤ }; 
            n = λ {  p → tt } }