Some types in the calculus of constructions

We can verify by Check that these types are admissible and of sort Type. One can also consider the formal rules of construction od dependant product, and do the verification manually.
The predicate associated to strictly monotonous functions from nat to nat has type (nat->nat)->Prop
The pointwise ordering on nat->nat :
  fun f g : nat-> nat => forall n:nat, f n <= g n

has type (nat->nat)->(nat->nat)->Prop
We can consider for instance a constant
boolean_matrix : nat->nat->Set
such that, if n and p are of type nat, the type
boolean_matrix n p
is the type of boolean matrices of height n and width p. This type has sort Set.

Going home
Pierre Castéran