\def\cprime{$'$}
\begin{thebibliography}{1}

\bibitem{Lambek}
J.~Lambek and P.~J. Scott.
\newblock {\em Introduction to higher order categorical logic}, volume~7 of
  {\em Cambridge Studies in Advanced Mathematics}.
\newblock Cambridge University Press, Cambridge, 1988.
\newblock Reprint of the 1986 original.

\bibitem{Streicher}
Thomas Streicher.
\newblock {\em Semantics of type theory}.
\newblock Progress in Theoretical Computer Science. Birkh\"auser Boston Inc.,
  Boston, MA, 1991.
\newblock Correctness, completeness and independence results, With a foreword
  by Martin Wirsing.

\end{thebibliography}