Agda Fizzbuzz w/o Standard Library

{-- fundamental types: equality, optional, natural --}
data _≡_ {A : Set} : (x y : A) → Set where
  refl : ∀ {x} → (x ≡ x)

data Maybe (A : Set) : Set where
  none : Maybe A
  some : A → Maybe A

data ℕ : Set where
  zer : ℕ
  suc : ℕ → ℕ

pattern `0 = zer
pattern `3 = suc (suc (suc `0))
pattern `5 = suc (suc `3)

{-- compare naturals --}
_==_ : ∀ (n m : ℕ) → Maybe (n ≡ m)
zer == zer = some refl
zer == suc m = none
suc n == zer = none
suc n == suc m with (n == m)
... | some refl = some refl
... | none = none
infix 2 _==_

{-- subtract naturals, returning 'none' if n < m --}
_-_ : (n m : ℕ) → Maybe ℕ
n     - zer = some n
zer   - suc m = none
suc n - suc m = n - m
infixr 3 _-_

{-- modulo; agda isn't convinced that this terminates --}
{-# TERMINATING #-}
_mod_ : (x n : ℕ) → ℕ
zer mod n = zer
suc x mod n with (suc x - n)
... | none = suc x
... | some d = d mod n
infix 4 _mod_ _div_

{-- is x divisible by n? --}
_div_ : (x n : ℕ) → Set
x div n = (x mod n) ≡ `0

{-- fizzbuzz type --}
data FB (n : ℕ) : Set where
  fizz : (n div `3) → FB n
  buzz : (n div `5) → FB n
  fizz-buzz : (n div `3) → (n div `5) → FB n
  number : FB n

{-- fizzbuzz algorithm --}
fb : (n : ℕ) → FB n
fb n with (n mod `3 == `0)
fb n | some p₃ with (n mod `5 == `0)
fb n | some p₃ | none    = fizz p₃
fb n | some p₃ | some p₅ = fizz-buzz p₃ p₅
fb n | none    with (n mod `5 == `0)
fb n | none    | some p₅ = buzz p₅
fb n | none    | none    = number