Library base
Abstract Parameters of PTS
a PTS depends on two sets that control typing of sorts and Π-types, and two other sets that define what is a sort and what is a variable.
Module Type term_sig.
Parameter Sorts : Set.
End term_sig.
Module Type pts_sig (X:term_sig).
Import X.
Parameter Sorts : Set.
End term_sig.
Module Type pts_sig (X:term_sig).
Import X.
Ax is used to type Sorts.
Rel is used to type Π-types.
To deal with variable binding, we use de Bruijn indexes: