Exercise: Encode multiplication as a type in Agda

multiplication.agda

-- This was an exercise: to encode _×_≡_ using _+_≡_
module Multiplication where

open import Data.Nat using (ℕ; suc; zero)

-- Addition encoded as a type
data _+_≡_ : ℕ → ℕ → ℕ → Set where
  zp : ∀ {n}                   →  zero  + n ≡ n
  sp : ∀ {m n k} →  m + n ≡ k  →  suc m + n ≡ suc k

-- Multiplication encoded as a type
data _×_≡_ : ℕ → ℕ → ℕ → Set where
  zm : ∀ {n}                                   →  zero  × n ≡ zero
  sm : ∀ {m n k i} →  m × n ≡ k  →  n + k ≡ i  →  suc m × n ≡ i

2×1≡2 : 2 × 1 ≡ 2
2×1≡2 = sm (sm zm (sp zp)) (sp zp)