\tableofcontents \section{Idea} We introduce a type theory over [[propositional logic]] as a dependent type theory. \section{See also} * [[dependent type theory]] * [[propositional logic]]