Universe polymorphism.

p.agda

module p where

open import Agda.Primitive

ℕ : (ℓ : _) → Set (lsuc ℓ)
ℕ ℓ = {x : Set ℓ} → (z : x) → (s : x → x) → x

zero : ∀ {ℓ} → ℕ ℓ
zero = λ z s → z

succ : ∀ {ℓ} → ℕ ℓ → ℕ ℓ
succ n = λ z s → s (n z s)

add : ∀ {ℓ} → ℕ (lsuc ℓ)  → ℕ ℓ → ℕ ℓ
add {ℓ = ℓ} a b = a {x = ℕ ℓ} b succ

p.idr

nat : Type
nat = (x : Type) -> x -> (x -> x) -> x

zero : nat
zero t z s = z

inc : nat -> nat
inc n t z s = s (n t z s)

-- This works
add : nat -> nat -> nat
add a b = a nat b inc

p.v

Definition nat : Type :=
  forall x, x -> (x -> x) -> x.
  
Definition zero : nat :=
  fun t z s => z.

Definition inc (n : nat) : nat :=
  fun t z s => s (n t z s).

(* This works *)
Definition add (a b : forall x, x -> (x -> x) -> x) : nat :=
  a nat b inc.

(* This doesn't *)
Definition add'' (a b : nat) : nat :=
  a nat b inc.

(* Error: Universe inconsistency. *)