idea

example.cat

induct _=_ {T} _ _ ≔
  rule reflexivity x. (x : T) -> (Refl x : x = x)
with module
  rule symmetry x y. x = y -> y = x ≔ λ (Refl x) → Refl x
  rule transitivity x y z. x = y -> y = z -> x = z ≔
    fun x-=-y y-=-z → (x-=-y)[ϕ y-=-z]
end

induct _×_ A B ≔
  rule pair x y. (x : A) -> (y : B) -> ('(x, y') : A × B) 
with module
  let π₁ (x, _) ≔ x
  let π₂ (_, y) ≔ y
end

induct Nat ≔
  ;; 0 is a natural number
  rule zero. 0 : Nat
  ;; if n is a natural number, S n is a natural number
  rule succ n. (n : Nat) -> (S n : nat)
with module
  codata _+_ ≔
    rule +-identity-right n. n + 0 = n
    rule +-identity-left m. 0 + m = m
    ;; we are using (S n) + m instead of the classical S (n + m) because
    ;; the former is tail-recursive
    rule +-succ-commutativity n m. n + S m = S n + m

  ;; beware: this is U+2212, not U+002D
  codata _−_ ≔
    rule −-identity-right n. n − 0 = n
    ;; XXX: we cannot omit [m] as it would prevent enforcing the higher
    ;; proposition [(m : Nat)]
    rule −-absorption-left m. 0 − m = 0
    rule −-succ-injectivity n m. S n − S m = n − m

  ;; beware: this is U+22C5
  codata _⋅_ ≔
    rule ⋅-absorption-right n. n ⋅ 0 = 0
    rule ⋅-absorption-left m. 0 ⋅ m = 0
    rule ⋅-succ-distributivity n m. n ⋅ S m = n + (n ⋅ m)

  codata divmod-tail _ _ _ ≔
    rule divmod-tail-absorption-right n quotient.
      divmod-tail quotient n 0 = (0, 0)
    rule divmod-tail-base-case quotient n m.
      (n < m) -> divmod-tail n m quotient = (quotient, n)
    rule divmod-tail-rec-case n m quotient.
      (n >= m) ->
        divmod-tail n m quotient = divmod-tail (n − m) m (S quotient)

  let divmod ≔ divmod-tail 0
  let _÷_ n m ≔ _×_.π₁ (divmod n m)
  let _%_ n m ≔ _×_.π₂ (divmod n m)
end