The limits of type theory: computation vs. interaction(researchblogs.cs.bham.ac.uk)

    data Bool : Set where
      true false : Bool

    if : ∀ {ℓ} {P : Bool → Set ℓ} (b : Bool) → P true → P false → P b
    if true  t f = t
    if false t f = f

    postulate Char : Set
    {-# BUILTIN CHAR Char #-}

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

    {-# BUILTIN NATURAL ℕ #-}

    ex₁ : ℕ
    ex₁ = if {P = λ b → if b ℕ Char} true 0 'a'

    infixr 5 _∷_

    data List {a} (A : Set a) : Set a where
      []  : List A
      _∷_ : A → List A → List A

    data HList : List Set → Set where
      []  : HList []
      _∷_ : ∀ {A As} → A → HList As → HList (A ∷ As)

    ex₂ : HList (ℕ ∷ Char ∷ (ℕ → ℕ) ∷ [])
    ex₂ = 1 ∷ 'a' ∷ suc ∷ []

  Inductive List (A: Set): Set :=
  | Nil: List A
  | Cons : A -> List A -> List A.

  CoInductive Stream (A: Set): Set :=
  | SCons: A -> Stream A -> Stream A.

  Fixpoint len {A: Set} (x: List A): nat :=
    match x with
     | Nil => 0
     | Cons _ y => 1 + len y
    end.

  CoFixpoint ones : Stream nat :=
    SCons nat 1 ones.