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

\bibitem{Aczel}
Peter Aczel.
\newblock A general church-rosser theorem.
\newblock {\em Unpublished manuscript}, 1978.

\bibitem{RezkCompletion}
Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman.
\newblock Univalent categories and the {R}ezk completion.
\newblock {\em Math. Structures Comput. Sci.}, 25(5):1010--1039, 2015.

\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{FPT}
Marcelo Fiore, Gordon Plotkin, and Daniele Turi.
\newblock Abstract syntax and variable binding (extended abstract).
\newblock In {\em 14th {S}ymposium on {L}ogic in {C}omputer {S}cience
  ({T}rento, 1999)}, pages 193--202. IEEE Computer Soc., Los Alamitos, CA,
  1999.

\bibitem{HM2007}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Modules over monads and linearity.
\newblock In {\em Logic, language, information and computation}, volume 4576 of
  {\em Lecture Notes in Comput. Sci.}, pages 218--237. Springer, Berlin, 2007.

\bibitem{NTS}
Vladimir Voevodsky.
\newblock Notes on type systems.
\newblock {\em \url{https://github.com/vladimirias/old_notes_on_type_systems}},
  2009--2012.

\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{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}