\def\cprime{$'$} \begin{thebibliography}{1} \bibitem{Bourbaki.Sets} Nicolas Bourbaki. \newblock {\em Theory of sets}. \newblock Elements of Mathematics (Berlin). Springer-Verlag, Berlin, 2004. \newblock Reprint of the 1968 English translation [Hermann, Paris; MR0237342]. \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{Lawvere} F.~William Lawvere. \newblock Functorial semantics of algebraic theories and some algebraic problems in the context of functorial semantics of algebraic theories. \newblock {\em Repr. Theory Appl. Categ.}, (5):1--121, 2004. \newblock Reprinted from Proc. Nat. Acad. Sci. U.S.A. {{\bf{5}}0} (1963), 869--872 [MR0158921] and {{\i}t Reports of the Midwest Category Seminar. II}, 41--61, Springer, Berlin, 1968 [MR0231882]. \bibitem{Cfromauniverse} Vladimir Voevodsky. \newblock A {C}-system defined by a universe category. \newblock {\em Theory Appl. Categ.}, 30:No. 37, 1181--1215, 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. \end{thebibliography}