In this paper, we add a simple form of dependent types—à la
Edinburgh LF [1]} and \(\lambda \textrm {LF}\)   [2]}—to \(\lambda ^{\triangleright \%}\) .
Types can be indexed by terms as in Vector in
Section  and \(\lambda \) -abstractions can be given
dependent function types of the form \(\Pi x:\tau . \sigma \)  but we do
not consider type operators (such as \(\texttt {list } \tau \) ) or
abstraction over type variables. We introduce kinds to classify
well-formed types and equivalences for kinds, types, and terms—as
in other dependent type systems—but we have to address a question
how the notion of stage (should) interact with kinds and types.
