\def\cprime{$'$} \begin{thebibliography}{1} \bibitem{FioreHur2009} Marcelo Fiore and Chung-Kil Hur. \newblock On the construction of free algebras for equational systems. \newblock {\em Theoret. Comput. Sci.}, 410(18):1704--1729, 2009. \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{Hamana2011} Makoto Hamana. \newblock Polymorphic abstract syntax via {G}rothendieck construction. \newblock In {\em Foundations of software science and computational structures}, volume 6604 of {\em Lecture Notes in Comput. Sci.}, pages 381--395. Springer, Heidelberg, 2011. \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{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{PowerTanaka} John Power and Miki Tanaka. \newblock Binding signatures for generic contexts. \newblock In {\em Typed lambda calculi and applications}, volume 3461 of {\em Lecture Notes in Comput. Sci.}, pages 308--323. Springer, Berlin, 2005. \end{thebibliography}