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

\bibitem{Aczel1978}
Peter Aczel.
\newblock The type theoretic interpretation of constructive set theory.
\newblock In {\em Logic {C}olloquium '77 ({P}roc. {C}onf., {W}roc\l aw, 1977)},
  volume~96 of {\em Stud. Logic Foundations Math.}, pages 55--66.
  North-Holland, Amsterdam-New York, 1978.

\bibitem{Adamek1974}
Ji{\v{r}}{\'{\i}} Ad{\'a}mek.
\newblock Free algebras and automata realizations in the language of
  categories.
\newblock {\em Comment. Math. Univ. Carolinae}, 15:589--602, 1974.

\bibitem{AM2016}
Benedikt Ahrens and Ralph Matthes.
\newblock Heterogeneous substitution systems revisited.
\newblock {\em https://arxiv.org/abs/1601.04299}, 2016.

\bibitem{AMM2016}
Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg.
\newblock From signatures to monads in unimath.
\newblock {\em https://arxiv.org/abs/1612.00693}, 2016.

\bibitem{AMM2017}
Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg.
\newblock Monads from multi-sorted binding signatures.
\newblock {\em http://benedikt-ahrens.de/multisorted.pdf}, 2017.

\bibitem{ACU}
Thorsten Altenkirch, James Chapman, and Tarmo Uustalu.
\newblock Monads need not be endofunctors.
\newblock In {\em Foundations of software science and computational
  structures}, volume 6014 of {\em Lecture Notes in Comput. Sci.}, pages
  297--311. Springer, Berlin, 2010.

\bibitem{ACU2}
Thorsten Altenkirch, James Chapman, and Tarmo Uustalu.
\newblock Monads need not be endofunctors.
\newblock {\em Logical Methods in Computer Science}, 11(1:3):1--40, 2015.

\bibitem{Barendregt}
H.~P. Barendregt.
\newblock {\em The lambda calculus}, volume 103 of {\em Studies in Logic and
  the Foundations of Mathematics}.
\newblock North-Holland Publishing Co., Amsterdam, revised edition, 1984.
\newblock Its syntax and semantics.

\bibitem{Barr1970}
Michael Barr.
\newblock Coequalizers and free triples.
\newblock {\em Math. Z.}, 116:307--322, 1970.

\bibitem{birkhoff1935}
Garrett Birkhoff.
\newblock On the structure of abstract algebras.
\newblock {\em Mathematical Proceedings of the Cambridge Philosophical
  Society}, 31(4):433–454, 1935.

\bibitem{Cartmell0}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ph.D. Thesis, Oxford University}, 1978.
\newblock \url{http://www.cs.ru.nl/~spitters/Cartmell.pdf}.

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

\bibitem{Church1932}
Alonzo Church.
\newblock A set of postulates for the foundation of logic.
\newblock {\em Ann. of Math. (2)}, 33(2):346--366, 1932.

\bibitem{Curry1930}
H.~B. Curry.
\newblock Grundlagen der {K}ombinatorischen {L}ogik.
\newblock {\em Amer. J. Math.}, 52(4):789--834, 1930.

\bibitem{FPT}
Marcelo Fiore, Gordon Plotkin, and Daniele Turi.
\newblock Abstract syntax and variable binding (extended abstract) ({W}arning:
  the paper uses the name ``presheaves'' for covariant functors to the category
  of sets).
\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{Garner}
Richard Garner.
\newblock Combinatorial structure of type dependency.
\newblock {\em J. Pure Appl. Algebra}, 219(6):1885--1914, 2015.

\bibitem{HM2010}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Modules over monads and initial semantics.
\newblock {\em Inform. and Comput.}, 208(5):545--564, 2010.

\bibitem{HM2012}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Nested abstract syntax in {C}oq.
\newblock {\em J. Automat. Reason.}, 49(3):409--426, 2012.

\bibitem{Hofmann}
Martin Hofmann.
\newblock Syntax and semantics of dependent types.
\newblock In {\em Semantics and logics of computation ({C}ambridge, 1995)},
  volume~14 of {\em Publ. Newton Inst.}, pages 79--130. Cambridge Univ. Press,
  Cambridge, 1997.

\bibitem{KLV1}
Chris Kapulkin, Peter~LeFanu Lumsdaine, and Vladimir Voevodsky.
\newblock The simplicial model of univalent foundations.
\newblock {\em Available at \url{http://arxiv.org/abs/1211.2851}}, 2012, 2014.

\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{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{MatthesUustalu}
Ralph Matthes and Tarmo Uustalu.
\newblock Substitution in non-wellfounded syntax with variable binding.
\newblock {\em Theoret. Comput. Sci.}, 327(1-2):155--174, 2004.

\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{Schonfinkel1924}
Moses Schönfinkel.
\newblock Über die bausteine der mathematischen logik.
\newblock {\em Math. Ann.}, 92:305 -- 316; Jbuch 50, 23, 1924.

\bibitem{2002Selinger}
Peter Selinger.
\newblock The lambda calculus is algebraic.
\newblock {\em J. Funct. Programming}, 12(6):549--566, 2002.

\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{FtoG}
Jean van Heijenoort.
\newblock {\em From {F}rege to {G}\"odel. {A} source book in mathematical
  logic, 1879--1931}.
\newblock Harvard University Press, Cambridge, Mass., 1967.

\bibitem{CMUtalk}
Vladimir Voevodsky.
\newblock The equivalence axiom and univalent models of type theory.
\newblock {\em \url{http://arxiv.org/abs/1402.5556}}, pages 1--11, February 4,
  2010.
\newblock \url{http://arxiv.org/abs/1402.5556}.

\bibitem{Cfromauniverse}
Vladimir Voevodsky.
\newblock A {C}-system defined by a universe category.
\newblock {\em Theory Appl. Categ.}, 30(37):1181--1215, 2015.
\newblock \url{http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf}.

\bibitem{UniMath2015}
Vladimir Voevodsky.
\newblock An experimental library of formalized mathematics based on the
  univalent foundations.
\newblock {\em Math. Structures Comput. Sci.}, 25(5):1278--1294, 2015.

\bibitem{fromunivwithpaths}
Vladimir Voevodsky.
\newblock Martin-{L}of identity types in the {C}-systems defined by a universe
  category.
\newblock {\em arXiv 1505.06446}, pages 1--51, 2015.
\newblock \url{http://arxiv.org/abs/1505.06446}, under review in Publication
  IHES.

\bibitem{CandJf}
Vladimir Voevodsky.
\newblock {C}-system of a module over a {Jf}-relative monad.
\newblock {\em arXiv 1602.00352}, pages 1--32, February 1, 2016.
\newblock \url{http://arxiv.org/abs/1602.00352}, under review in Pure and
  Applied Algebra.

\bibitem{fromunivwithPiI}
Vladimir Voevodsky.
\newblock Products of families of types and {$(\Pi,\lambda)$}-structures on
  {C}-systems.
\newblock {\em Theory Appl. Categ.}, 31:Paper No. 36, 1044--1094, 2016.
\newblock \url{http://www.tac.mta.ca/tac/volumes/31/36/31-36.pdf}.

\bibitem{Csubsystems}
Vladimir Voevodsky.
\newblock Subsystems and regular quotients of {C}-systems.
\newblock In {\em A panorama of mathematics: pure and applied}, volume 658 of
  {\em Contemp. Math.}, pages 127--137. Amer. Math. Soc., Providence, RI, 2016.
\newblock prepublication version in \url{http://arxiv.org/abs/1406.7413}.

\bibitem{fromunivwithPiII}
Vladimir Voevodsky.
\newblock The {$(\Pi, \lambda)$}-structures on the {C}-systems defined by
  universe categories.
\newblock {\em Theory Appl. Categ.}, 32:Paper No. 4, 113--121, 2017.
\newblock \url{http://www.tac.mta.ca/tac/volumes/32/4/32-04.pdf}.

\bibitem{CandJfsubquot}
Vladimir Voevodsky.
\newblock The regular sub-quotients of the {C}-systems {$CC(\RR,\LM)$}.
\newblock {\em In preparation}, 2017.

\bibitem{UniMath}
Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et~al.
\newblock {\em UniMath} - a library of formalized mathematics.
\newblock Available at \url{https://github.com/UniMath}.

\bibitem{Zsido}
Julianna Zsido.
\newblock {\em {Typed Abstract Syntax}}.
\newblock Theses, {Universit{\'e} Nice Sophia Antipolis}, June 2010.

\end{thebibliography}