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

\bibitem[Car86]{Cartmell1}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ann. Pure Appl. Logic}, 32(3):209--243, 1986.

\bibitem[HS98]{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[May68]{Ma}
Peter May.
\newblock {\em Simplicial objects in algebraic topology}.
\newblock Van Nostrand, 1968.

\bibitem[PV07]{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[Str91]{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}