# 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