Minimal agda definition for induction on natural numbers. (I realize that it's actually just dependent foldr).

NatInduction.agda

module NatInduction where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ 

ℕ-ind : (prop        : ℕ → Set)
      → (zero_proof  : prop zero)
      → (ind_hyp     : ∀ n → prop n → prop (suc n))
      → (n           : ℕ)
      → prop n
ℕ-ind prop zp hyp zero = zp
ℕ-ind prop zp hyp (suc n) = hyp n (ℕ-ind prop zp hyp n)