{-# OPTIONS --without-K #-}
module sets.nat.core where

open import level
open import decidable
open import equality.core
open import function.core
open import function.isomorphism.core
open import sets.empty

infixr 8 _^_
infixl 7 _*_
infixl 6 _+_

data  : Set where
  zero : 
  suc  :   

{-# BUILTIN NATURAL     #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

pred :   
pred zero    = zero
pred (suc n) = n

_+_ :     
zero  + n = n
suc m + n = suc (m + n)

_*_ :     
0 * n = zero
suc m * n = n + m * n

_^_ :     
n ^ 0 = 1
n ^ (suc m) = n * (n ^ m)

suc-inj : injective suc
suc-inj = ap pred

_≟_ : (a b : )  Dec (a  b)
zero   zero  = yes refl
zero   suc _ = no  ())
suc _  zero  = no  ())
suc a  suc b with a  b
suc a  suc b | yes a≡b = yes $ ap suc a≡b
suc a  suc b | no ¬a≡b = no $  sa≡sb  ¬a≡b (ap pred sa≡sb))