Exercise 4.1

1. (ℕ → ℕ) → Prop

Well formed type:

(ℕ : Set) ∈ E ∪ Γ E, Γ ⊢ ℕ : Set Var (ℕ : Set) ∈ E ∪ Γ E, Γ ⊢ ℕ : Set Var
E, Γ ⊢ ℕ → ℕ : Set

Prod-Set

                                         (Prop : Type) ∈ E ∪ Γ E, Γ ⊢ Prop : Type Var

E, Γ ⊢ (ℕ → ℕ) → Prop : Type

Prod-Dep

It is the type of the statement: A given function f (from nat to nat) is monotone.

2. (ℕ → ℕ) → (ℕ → ℕ) → Prop

It is the type of the statement:

For two given functinos f and g (from nat to nat) f is the inverse of g

3. ℕ → ℕ → Set

It is the type of a matrix-type constructor. Given two naturals n and m we form a matrix of dimension n × m.