module Chapter5.Container.Examples.Nat where

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

open import Chapter5.Container

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