(** * 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. *) (** ** Sorts and Variables Sorts can be anything we want: *) Module Type term_sig. Parameter Sorts : Set. End term_sig. Module Type pts_sig (X:term_sig). Import X. (** [Ax] is used to type [Sorts]. *) Parameter Ax : Sorts -> Sorts -> Prop. (** [Rel] is used to type Π-types. *) Parameter Rel : Sorts -> Sorts -> Sorts -> Prop. End pts_sig. (** To deal with variable binding, we use de Bruijn indexes: *) Definition Vars := nat.