{-# OPTIONS --safe #-}

module Data.Nat where

open import Agda.Builtin.Nat using (suc; zero; _+_) renaming (Nat to ℕ) public

open import Agda.Builtin.FromNat
open import Data.Unit

instance
  numberNat : Number ℕ
  numberNat = record
    { Constraint = λ _ → ⊤
    ; fromNat    = λ n → n
    }

open import Data.Bool

open import Agda.Builtin.Nat using (mod-helper; div-helper; _==_)

--           n mod (suc m) = mod-helper 0 m n m
-- n mod 2 = n mod (suc 1) = mod-helper 0 1 n 1

even : ℕ → Bool
even n = mod-helper 0 1 n 1 == 0

div2 : ℕ → ℕ
div2 n = div-helper 0 1 n 1

open import Discrete
open import Path

module DiscreteNat where
  opaque
    _≡ᴮ_ : ℕ → ℕ → Bool
    _≡ᴮ_ = _==_

    complete : ∀ (x) → T (x ≡ᴮ x)
    complete zero = tt
    complete (suc n) = complete n

    sound : ∀ x y → T (x ≡ᴮ y) → x ≡ y
    sound zero zero xy = refl
    sound (suc x) (suc y) xy = cong suc (sound x y xy)

instance
  opaque
    discreteNat : IsDiscrete ℕ
    discreteNat = record { _≟_ = from-bool-eq (record { DiscreteNat }) }

open import HLevels
open import Discrete.IsSet

isSetℕ : isSet ℕ
isSetℕ = Discrete→isSet _≟_