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