Factorial with types and values in Agda.

Fact.agda

module Fact where

open import Data.Nat

-- Fact at the type-level
data Fact : ℕ → ℕ → Set where
  factZero : Fact 0 1
  factSuc : {n m : ℕ} → Fact n m → Fact (suc n) ((suc n) * m)

-- Value level
fact : ℕ → ℕ
fact 0 = 1
fact (suc n) = (suc n) * (fact n)

-- Check that they're the same
getFact : ∀ n → Fact n (fact n)
getFact 0 = factZero
getFact (suc n) = factSuc (getFact n)