TTinTT.lagda

%if False
\begin{code}
module TTinTT where

open import OTT public
\end{code}
%endif

A while ago, we defined the simply typed $\lambda$-calculus as a syntax of
well scoped, well typed terms. Can we do the same for a dependently typed
calculus? Yes and no, but not necessarily in that order.