import NNG.Metadata
import NNG.MyNat.Addition

namespace MyNat

-- TODO: Do we need these instances?
-- (kmb) I wanted to introduce these instances as "collectibles" as
-- one went through the "main route" from addition world to power
-- world. If you could make some extra window with those collectibles
-- in, and whenever you have an instance sorry-free it awards you
-- the collectible, that would be great! These things were just
-- precisely the oddball (to my eyes) classes which nat was an instance of,
-- but I think they would make great collectibles.

-- instance addSemigroup : AddSemigroup ℕ :=
-- {
--   zero := 0

-- }
-- MyNat.addMonoid        -- (after level 2)
-- MyNat.addCommSemigroup -- (after level 4)
-- MyNat.addCommMonoid    -- (after level 4)