[Agda] More universe polymorphism

[Nils Anders Danielsson]

On 2013-06-28 01:09, Darryl McAdams wrote:
> I've certainly run into issues with levels. A good example is an
> implementation of Scott/Church encodings. You can define the encoding,
> but trying to define simple things like addition becomes difficult if
> not impossible, from what I can tell.

Are you referring to some kind of universe-polymorphic Church numerals?
The basic encoding works fine (for addition, at least):

module Church where

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

Cℕ : Set₁
Cℕ = {A : Set} → A → (A → A) → A

toℕ : Cℕ → ℕ
toℕ n = n zero suc

fromℕ : ℕ → Cℕ
fromℕ zero    = λ z s → z
fromℕ (suc n) = λ z s → s (fromℕ n z s)

toℕ-fromℕ : ∀ n → toℕ (fromℕ n) ≡ n
toℕ-fromℕ zero    = refl
toℕ-fromℕ (suc n) = cong suc (toℕ-fromℕ n)

_+_ : Cℕ → Cℕ → Cℕ
m + n = λ z s → m (n z s) s

+-correct : ∀ m n → toℕ (fromℕ m + fromℕ n) ≡ m Data.Nat.+ n
+-correct zero    n = toℕ-fromℕ n
+-correct (suc m) n = cong suc (+-correct m n)

-- 
/NAD