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

\bibitem{Abbott1}
Michael Abbott, Thorsten Altenkirch, and Neil Ghani.
\newblock Categories of containers.
\newblock In {\em In Proceedings of Foundations of Software Science and
  Computation Structures}, 2003.

\bibitem{Blanqui1}
Fr{\'e}d{\'e}ric Blanqui.
\newblock Type theory and rewritting.
\newblock In {\em Ph. D. Thesis}, pages 1--139. Orsay, 2001.

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

\bibitem{deBruijn}
N.~G. de~Bruijn.
\newblock Lambda calculus notation with nameless dummies, a tool for automatic
  formula manipulation, with application to the {C}hurch-{R}osser theorem [
  {MR}0321704 (48 \#71)].
\newblock In {\em Selected papers on {A}utomath}, volume 133 of {\em Stud.
  Logic Found. Math.}, pages 375--388. North-Holland, Amsterdam, 1994.

\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{Mohring1}
Christine Paulin-Mohring.
\newblock Inductive definitions in the system {C}oq; rules and properties.
\newblock In {\em Typed lambda calculi and applications ({U}trecht, 1993)},
  volume 664 of {\em Lecture Notes in Comput. Sci.}, pages 328--345. Springer,
  Berlin, 1993.

\bibitem{Pitts}
Andrew~M. Pitts.
\newblock {\em Nominal sets}, volume~57 of {\em Cambridge Tracts in Theoretical
  Computer Science}.
\newblock Cambridge University Press, Cambridge, 2013.
\newblock Names and symmetry in computer science.

\bibitem{Quillen2}
Daniel~G. Quillen.
\newblock The geometric realization of a {K}an fibration is a {S}erre
  fibration.
\newblock {\em Proc. Amer. Math. Soc.}, 19:1499--1500, 1968.

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

\bibitem{Werner}
B.~Werner.
\newblock Une théorie des constructions inductives.
\newblock In {\em Thèse de Doctorat}, 1994.

\end{thebibliography}