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

\bibitem{BCH}
Marc Bezem, Thierry Coquand, and Simon Huber.
\newblock A model of type theory in cubical sets.
\newblock {\em \url{http://www.cse.chalmers.se/~coquand/mod1.pdf}}, 2014.

\bibitem{Cartmell0}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ph.D. Thesis, Oxford University}, 1978.
\newblock \url{https://uf-ias-2012.wikispaces.com/Semantics+of+type+theory}.

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

\bibitem{Dybjer}
Peter Dybjer.
\newblock Internal type theory.
\newblock In {\em Types for proofs and programs ({T}orino, 1995)}, volume 1158
  of {\em Lecture Notes in Comput. Sci.}, pages 120--134. Springer, Berlin,
  1996.

\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{MLTT73}
Per Martin-L{\"o}f.
\newblock An intuitionistic theory of types: predicative part.
\newblock In {\em Logic {C}olloquium '73 ({B}ristol, 1973)}, pages 73--118.
  Studies in Logic and the Foundations of Mathematics, Vol. 80. North-Holland,
  Amsterdam, 1975.

\bibitem{MLTT79}
Per Martin-L{\"o}f.
\newblock Constructive mathematics and computer programming.
\newblock In {\em Logic, methodology and philosophy of science, {VI}
  ({H}annover, 1979)}, volume 104 of {\em Stud. Logic Found. Math.}, pages
  153--175. North-Holland, Amsterdam, 1982.

\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{vandenBergGarner2011}
Benno van~den Berg and Richard Garner.
\newblock Types are weak {$\omega$}-groupoids.
\newblock {\em Proc. Lond. Math. Soc. (3)}, 102(2):370--394, 2011.

\bibitem{BergandGarner}
Benno van~den Berg and Richard Garner.
\newblock Topological and simplicial models of identity types.
\newblock {\em ACM Trans. Comput. Log.}, 13(1):Art. 3, 44, 2012.

\bibitem{CMUtalk}
Vladimir Voevodsky.
\newblock The equivalence axiom and univalent models of type theory.
\newblock {\em arXiv 1402.5556}, pages 1--11, 2010.

\bibitem{SRF}
Vladimir Voevodsky.
\newblock Simplicial radditive functors.
\newblock {\em J. K-Theory}, 5(2):201--244, 2010.

\bibitem{Cfromauniverse}
Vladimir Voevodsky.
\newblock A {C-system} defined by a universe category.
\newblock {\em arXiv 1409.7925, submitted}, pages 1--7, 2014.

\bibitem{Cofamodule}
Vladimir Voevodsky.
\newblock {C-system} of a module over a monad on sets.
\newblock {\em arXiv 1407.3394, submitted}, pages 1--20, 2014.

\bibitem{fromunivwithPi}
Vladimir Voevodsky.
\newblock Products of families of types in the {C-systems} defined by a
  universe category.
\newblock {\em arXiv 1503.07072, submitted}, pages 1--30, 2015.

\bibitem{Csubsystems}
Vladimir Voevodsky.
\newblock Subsystems and regular quotients of {C-systems}.
\newblock In {\em Conference on Mathematics and its Applications, (Kuwait City,
  2014)}, number to appear, pages 1--11, 2015.

\bibitem{WarrenThesisProsp}
Michael Warren.
\newblock Homotopy models of intensional type theory.
\newblock {\em \url{http://mawarren.net/papers/prospectus.pdf}}, 2006.

\bibitem{WarrenThesis}
Michael Warren.
\newblock Homotopy theoretic aspects of constructive type theory.
\newblock {\em \url{http://mawarren.net/papers/phd.pdf}}, 2008.

\bibitem{Warreninfty}
Michael~A. Warren.
\newblock The strict {$\omega$}-groupoid interpretation of type theory.
\newblock In {\em Models, logics, and higher-dimensional categories}, volume~53
  of {\em CRM Proc. Lecture Notes}, pages 291--340. Amer. Math. Soc.,
  Providence, RI, 2011.

\end{thebibliography}