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

\bibitem{Barendregt92}
H.~P. Barendregt.
\newblock Lambda calculi with types.
\newblock In {\em Handbook of logic in computer science, {V}ol.\ 2}, volume~2
  of {\em Handb. Log. Comput. Sci.}, pages 117--309. Oxford Univ. Press, New
  York, 1992.

\bibitem{Hofmann1}
Martin Hofmann and Thomas Streicher.
\newblock The groupoid interpretation of type theory.
\newblock In {\em Twenty-five years of constructive type theory ({V}enice,
  1995)}, volume~36 of {\em Oxford Logic Guides}, pages 83--111. Oxford Univ.
  Press, New York, 1998.

\bibitem{Jacobs1}
Bart Jacobs.
\newblock {\em Categorical logic and type theory}, volume 141 of {\em Studies
  in Logic and the Foundations of Mathematics}.
\newblock North-Holland Publishing Co., Amsterdam, 1999.

\bibitem{Ma}
Peter May.
\newblock {\em Simplicial objects in algebraic topology}.
\newblock Van Nostrand, 1968.

\bibitem{Palmgren1}
E.~Palmgren and S.~J. Vickers.
\newblock Partial horn logic and {C}artesian categories.
\newblock {\em Ann. Pure Appl. Logic}, 145(3):314--353, 2007.

\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}