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