module blog_arithmetic where
  open import EqualityBase public

  data Nat : 𝓤₀ ̇ where
    zero : Nat
    succ : Nat → Nat

  _⊞_ : Nat → Nat → Nat
  zero     ⊞ n = n
  (succ m) ⊞ n = succ (m ⊞ n)

  _⊠_ : Nat → Nat → Nat
  zero     ⊠ n = zero
  (succ m) ⊠ n = (m ⊠ n) ⊞ n

  infixl 20 _⊞_
  infixl 21 _⊠_

  pluszero : (n : Nat) → (n ⊞ zero) ≡ n
  pluszero zero     = refl zero
  pluszero (succ n) = ap succ (pluszero n)

  one : Nat
  one = succ zero

  succ+1 : (n : Nat) → succ n ≡ (n ⊞ one)
  succ+1 zero     = refl one
  succ+1 (succ n) = ap succ (succ+1 n)

  plus-assoc : (m n p : Nat) → (m ⊞ (n ⊞ p)) ≡ (m ⊞ n ⊞ p)
  plus-assoc zero n p     = refl (n ⊞ p)
  plus-assoc (succ m) n p = ap succ (plus-assoc m n p)

  m-plus-Sn : (m n : Nat) → (m ⊞ succ n) ≡ succ (m ⊞ n)
  m-plus-Sn zero n     = refl (succ n)
  m-plus-Sn (succ m) n = ap succ (m-plus-Sn m n)

  plus-comm : (m n : Nat) → (m ⊞ n) ≡ (n ⊞ m)
  plus-comm zero n     = (pluszero n) ⁻¹
  plus-comm (succ m) n = (ap succ (plus-comm m n)) ∙ ((m-plus-Sn n m) ⁻¹)