Library PTSATR.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.

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.