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