\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{{n{L}a}16}

\bibitem[Awo06]{awodey:cat-thy}
Steve Awodey.
\newblock {\em Category theory}, volume~49 of {\em Oxford Logic Guides}.
\newblock The Clarendon Press Oxford University Press, New York, 2006.

\bibitem[Bae04]{baez:why-ncats}
John Baez.
\newblock Why $n$-categories?
\newblock \url{http://www.math.ucr.edu/home/baez/n_categories/why.pdf}, 2004.

\bibitem[Bat98]{batanin:cptd-fin}
M.A. Batanin.
\newblock Computads for finitary monads on globular sets, 1998.

\bibitem[BKP89]{bkp:2dmonads}
R.~Blackwell, G.~M. Kelly, and A.~J. Power.
\newblock Two-dimensional monad theory.
\newblock {\em J. Pure Appl. Algebra}, 59(1):1--41, 1989.

\bibitem[Bur71]{burroni:t-cats}
Albert Burroni.
\newblock {$T$}-cat\'egories (cat\'egories dans un triple).
\newblock {\em Cahiers Topologie G\'eom. Diff\'erentielle}, 12:215--321, 1971.

\bibitem[Cro12]{crole:alpha}
Roy~L. Crole.
\newblock Alpha equivalence equalities.
\newblock {\em Theoretical Computer Science}, 433:1 -- 19, 2012.

\bibitem[CS10]{cs:multicats}
G.S.H. Cruttwell and Michael Shulman.
\newblock A unified framework for generalized multicategories.
\newblock {\em Theory Appl. Categ.}, 24:580--655, 2010.
\newblock arXiv:0907.2460.

\bibitem[Day70]{day:closed}
Brian Day.
\newblock On closed categories of functors.
\newblock In {\em Reports of the Midwest Category Seminar, IV}, Lecture Notes
  in Mathematics, Vol. 137, pages 1--38. Springer, Berlin, 1970.

\bibitem[Do{\v s}99]{dosen:cutelim-cats}
Kosta Do{\v s}en.
\newblock {\em Cut elimination in categories}.
\newblock Springer, 1999.

\bibitem[DP07]{dp:relevant-cats}
Kosta Do{\v s}en and Zoran Petri{\'c}.
\newblock Relevant categories and partial functions.
\newblock {\em Publications de l'Institut Math{\'e}matique, Nouvelle
  S{\'e}rie}, 82(96):17--23, 2007.

\bibitem[Gar10]{garner:hom-hcat}
Richard Garner.
\newblock Homomorphisms of higher categories.
\newblock {\em Advances in Mathematics}, In Press, Corrected Proof:--, 2010.

\bibitem[Gol84]{goldblatt:topoi}
Robert Goldblatt.
\newblock {\em Topoi}, volume~98 of {\em Studies in Logic and the Foundations
  of Mathematics}.
\newblock North-Holland Publishing Co., Amsterdam, second edition, 1984.
\newblock The categorial analysis of logic.

\bibitem[GP99]{gp:asib}
M.~J. Gabbay and A.~M. Pitts.
\newblock A new approach to abstract syntax involving binders.
\newblock In {\em Proceedings of the 14th Annual Symposium on Logic in Computer
  Science, LICS'99}, pages 214--224, Trento, Italy, 1999. IEEE Computer Society
  Press.

\bibitem[GP02]{gp:aswvb}
M.~J. Gabbay and A.~M. Pitts.
\newblock A new approach to abstract syntax with variable binding.
\newblock {\em Formal Aspects of Computing}, 13:341--363, 2002.

\bibitem[Her00]{hermida:multicats}
Claudio Hermida.
\newblock Representable multicategories.
\newblock {\em Adv. Math.}, 151(2):164--225, 2000.

\bibitem[Her01]{hermida:coh-univ}
Claudio Hermida.
\newblock From coherent structures to universal properties.
\newblock {\em J. Pure Appl. Algebra}, 165(1):7--61, 2001.

\bibitem[Jac99]{jacobs:cltt}
Bart Jacobs.
\newblock {\em Categorical Logic and Type Theory}.
\newblock Number 141 in Studies in Logic and the Foundations of Mathematics.
  North Holland, Amsterdam, 1999.

\bibitem[Joh77]{ptj:topos-theory}
Peter~T. Johnstone.
\newblock {\em Topos theory}.
\newblock Academic Press [Harcourt Brace Jovanovich Publishers], London, 1977.
\newblock London Mathematical Society Monographs, Vol. 10.

\bibitem[Joh02]{ptj:elephant}
Peter~T. Johnstone.
\newblock {\em Sketches of an Elephant: A Topos Theory Compendium: Volumes 1
  and 2}.
\newblock Number~43 in Oxford Logic Guides. Oxford Science Publications, 2002.

\bibitem[JS91]{js:geom-tenscalc-i}
Andr{\'e} Joyal and Ross Street.
\newblock The geometry of tensor calculus. {I}.
\newblock {\em Adv. Math.}, 88(1):55--112, 1991.

\bibitem[Lam69]{lambek:dedsys-ii}
Joachim Lambek.
\newblock Deductive systems and categories. {II}. {S}tandard constructions and
  closed categories.
\newblock In {\em Category {T}heory, {H}omology {T}heory and their
  {A}pplications, {I} ({B}attelle {I}nstitute {C}onference, {S}eattle, {W}ash.,
  1968, {V}ol. {O}ne)}, pages 76--122. Springer, Berlin, 1969.

\bibitem[Lam80]{lambek:stlc-ccc}
Joachim Lambek.
\newblock From $\lambda$-calculus to cartesian closed categories.
\newblock {\em To HB Curry: essays on combinatory logic, lambda calculus and
  formalism}, pages 375--402, 1980.

\bibitem[Law63]{lawvere:functsem}
F.~William Lawvere.
\newblock Functorial semantics of algebraic theories.
\newblock {\em Proc. Nat. Acad. Sci. U.S.A.}, 50:869--872, 1963.

\bibitem[Law70]{lawvere:comprehension}
F.~William Lawvere.
\newblock Equality in hyperdoctrines and comprehension schema as an adjoint
  functor.
\newblock In {\em Applications of Categorical Algebra (Proc. Sympos. Pure
  Math., Vol. XVII, New York, 1968)}, pages 1--14. Amer. Math. Soc.,
  Providence, R.I., 1970.

\bibitem[Law06]{lawvere:adjointness}
F.~William Lawvere.
\newblock Adjointness in foundations.
\newblock {\em Repr. Theory Appl. Categ.}, (16):1--16 (electronic), 2006.
\newblock Reprinted from Dialectica {\bf 23} (1969).

\bibitem[Lei04]{leinster:higher-opds}
Tom Leinster.
\newblock {\em Higher operads, higher categories}, volume 298 of {\em London
  Mathematical Society Lecture Note Series}.
\newblock Cambridge University Press, Cambridge, 2004.

\bibitem[Lei14]{leinster:cat-thy}
Tom Leinster.
\newblock {\em Basic category theory}.
\newblock Cambridge University Press, 2014.

\bibitem[LS88]{ls:hocl}
J.~Lambek and P.~J. Scott.
\newblock {\em Introduction to Higher-Order Categorical Logic}, volume~7 of
  {\em Cambridge Studies in Advanced Mathematics}.
\newblock Cambridge University Press, 1988.

\bibitem[LS16]{ls:1var-adjoint-logic}
Daniel Licata and Michael Shulman.
\newblock Adjoint logic with a 2-category of modes.
\newblock LFCS '16. Available at
  \url{http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf}, 2016.

\bibitem[May72]{may:goils}
J.~Peter May.
\newblock {\em The geometry of iterated loop spaces}.
\newblock Springer-Verlag, Berlin, 1972.
\newblock Lectures Notes in Mathematics, Vol. 271.

\bibitem[McL92]{mclarty:ecat-etop}
Colin McLarty.
\newblock {\em Elementary categories, elementary toposes}, volume~21 of {\em
  Oxford Logic Guides}.
\newblock The Clarendon Press Oxford University Press, New York, 1992.
\newblock Oxford Science Publications.

\bibitem[ML98]{maclane}
Saunders Mac~Lane.
\newblock {\em Categories For the Working Mathematician}, volume~5 of {\em
  Graduate Texts in Mathematics}.
\newblock Springer, second edition, 1998.

\bibitem[MLM94]{mm:shv-gl}
Saunders Mac~Lane and Ieke Moerdijk.
\newblock {\em Sheaves in geometry and logic: a first introduction to topos
  theory}.
\newblock Universitext. Springer-Verlag, New York, 1994.
\newblock Corrected reprint of the 1992 edition.

\bibitem[MR77]{mr:focl}
M.~Makkai and G.E. Reyes.
\newblock {\em First Order Categorical Logic}, volume 611 of {\em Lecture Notes
  in Mathematics}.
\newblock Springer-Verlag, 1977.

\bibitem[{n{L}a}16]{nlab:computad}
{n{L}ab authors}.
\newblock computad.
\newblock \url{http://ncatlab.org/nlab/show/computad}, Jul 2016.

\bibitem[PG00]{pg:freshml}
A.~M. Pitts and M.~J. Gabbay.
\newblock A metalanguage for programming with bound names modulo renaming.
\newblock In R.~Backhouse and J.~N. Oliveira, editors, {\em Mathematics of
  Program Construction. 5th International Conference, MPC2000}, volume 1837 of
  {\em Lecture Notes in Computer Science}, pages 230--255. Springer, July 2000.

\bibitem[Sel11]{selinger:graphical}
Peter Selinger.
\newblock A survey of graphical languages for monoidal categories.
\newblock In Bob Coeke, editor, {\em New Structures for Physics}, chapter~4.
  Springer, 2011.
\newblock Available at
  \url{http://www.mscs.dal.ca/~selinger/papers.html\#graphical} and
  arXiv:0908.3347.

\bibitem[SL{\etalchar{+}}10]{shulman:what-is-a-theory}
Michael Shulman, Peter~LeFanu Lumsdaine, et~al.
\newblock What is a theory?
\newblock Blog post and discussion available at
  \url{https://golem.ph.utexas.edu/category/2010/07/what_is_a_theory.html},
  2010.

\bibitem[Str83]{street:absolute}
Ross Street.
\newblock Absolute colimits in enriched categories.
\newblock {\em Cahiers Topologie G\'eom. Diff\'erentielle}, 24(4):377--379,
  1983.

\bibitem[Wad15]{wadler:pat}
Philip Wadler.
\newblock Propositions as types.
\newblock {\em Communications of the ACM}, 2015.
\newblock
  \url{http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf}.

\bibitem[Wyl91]{wyler:quasitopoi}
Oswald Wyler.
\newblock {\em Lecture notes on topoi and quasitopoi}.
\newblock World Scientific, 1991.

\end{thebibliography}