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

\bibitem{AwodeyNM}
Steve Awodey.
\newblock Natural models of homotopy type theory.
\newblock {\em \url{http://arxiv.org/abs/1406.3219}}, 2014.

\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{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{Csubsystems}
Vladimir Voevodsky.
\newblock Subsystems and regular quotients of {C-systems}.
\newblock {\em \url{http://arxiv.org/abs/1406.7413}}, 2014.

\bibitem{Bsystems}
Vladimir Voevodsky.
\newblock B-systems.
\newblock {\em \url{http://arxiv.org/abs/1410.5389}}, October 2014.

\end{thebibliography}
