{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:00:08Z","timestamp":1773097208762,"version":"3.50.1"},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2021,10,18]],"date-time":"2021-10-18T00:00:00Z","timestamp":1634515200000},"content-version":"unspecified","delay-in-days":17,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a <jats:italic>presentation<\/jats:italic> \u03a3 of a generalized algebraic theory and the associated category <jats:bold>CwF<\/jats:bold><jats:sub>\u03a3<\/jats:sub> of small cwfs with a \u03a3-structure and cwf-morphisms that preserve \u03a3-structure on the nose. Our definition refers to the purely semantic notion of <jats:italic>uniform family<\/jats:italic> of contexts, types, and terms in <jats:bold>CwF<\/jats:bold><jats:sub>\u03a3<\/jats:sub>. Furthermore, we show how to syntactically construct an initial cwf with a \u03a3-structure. This result can be viewed as a generalization of Birkhoff\u2019s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer\u2019s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-L\u00f6f type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.<\/jats:p>","DOI":"10.1017\/s0960129521000268","type":"journal-article","created":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T10:06:02Z","timestamp":1634637962000},"page":"1006-1023","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":4,"title":["On generalized algebraic theories and categories with families"],"prefix":"10.1017","volume":"31","author":[{"given":"Marc","family":"Bezem","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-5153","authenticated-orcid":false,"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4043-5204","authenticated-orcid":false,"given":"Peter","family":"Dybjer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4091-6334","authenticated-orcid":false,"given":"Mart\u00edn","family":"Escard\u00f3","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,10,18]]},"reference":[{"key":"S0960129521000268_ref24","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316071"},{"key":"S0960129521000268_ref10","unstructured":"Cartmell, J. (2018). Generalised algebraic axiomatisations of contextual categories. https:\/\/www.researchgate.net\/publication\/325763538_Generalised_Algebraic_Axiomatisations_of_Contextual_Categories."},{"key":"S0960129521000268_ref18","unstructured":"Forsberg, F. N. and Setzer, A. (2010). Inductive-inductive definitions. In Dawar, A. and Veith, H. , editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23\u201327, 2010. Proceedings, vol. 6247. Lecture Notes in Computer Science. Springer, 454\u2013468."},{"key":"S0960129521000268_ref11","unstructured":"Castellan, S. , Clairambault, P. and Dybjer, P. (2015). Undecidability of equality in the free locally cartesian closed category. In 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1\u20133, 2015, Warsaw, Poland, 138\u2013152."},{"key":"S0960129521000268_ref7","unstructured":"Brunerie, G. (2019). A formalization of the initiality conjecture in Agda. Slides from a talk about joint work with Menno de Boer, Peter Lumsdaine, and Anders M\u00f6rtberg, at HoTT, Pittsburgh, CMU."},{"key":"S0960129521000268_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000881"},{"key":"S0960129521000268_ref5","doi-asserted-by":"crossref","unstructured":"Awodey, S. , Frey, J. and Speight, S. (2018). Impredicative encodings of (higher) inductive types. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2018). New York, NY, USA, Association for Computing Machinery.","DOI":"10.1145\/3209108.3209130"},{"key":"S0960129521000268_ref32","unstructured":"Uemura, T. (2019). A general framework for the semantics of type theory. ArXiv, abs\/1904.04097."},{"key":"S0960129521000268_ref26","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0960129521000268_ref1","unstructured":"The Agda wiki. http:\/\/appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php."},{"key":"S0960129521000268_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"S0960129521000268_ref23","volume-title":"CPHC\/BCS distinguished dissertations","author":"Hofmann","year":"1997"},{"key":"S0960129521000268_ref13","doi-asserted-by":"crossref","unstructured":"Castellan, S. , Clairambault, P. and Dybjer, P. (2021). Categories with families: Unityped, simply typed, and dependently typed. In: Casadio, C. and Scott, P. J. (eds.) Joachim Lambek: The interplay of Mathematics, Logic, and Linguistics, Outstanding Contributions to Logic, Editor-in-Chief: Sven-Ove Hansson. vol. 20. Springer.","DOI":"10.1007\/978-3-030-66545-6_5"},{"key":"S0960129521000268_ref34","unstructured":"Voevodsky, V. (2017). Models, interpretations and the initiality conjectures. Notes from a lecture at the 2017 Logic Colloquium in Stockholm, special session on Category Theory and Type Theory in honor of Per Martin-Lf on his 75th birthday. https:\/\/www.math.ias.edu\/Voevodsky\/files\/files-annotated\/Dropbox\/Unfinished_papers\/Type_systems\/Notes_on_Type_Systems\/2017_LC_Martin-Lof_special_session\/BSL_extended_abstract.pdf."},{"key":"S0960129521000268_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.03.003"},{"key":"S0960129521000268_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_10"},{"key":"S0960129521000268_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"S0960129521000268_ref30","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1037"},{"key":"S0960129521000268_ref8","unstructured":"Cartmell, J. (1978). Generalized Algebraic Theories and Contextual Categories. D. Phil., Oxford University."},{"key":"S0960129521000268_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"S0960129521000268_ref19","volume-title":"Abelian Categories","author":"Freyd","year":"1964"},{"key":"S0960129521000268_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"S0960129521000268_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_7"},{"key":"S0960129521000268_ref27","unstructured":"Martin-L\u00f6f, P. (1992). Substitution calculus. Notes from a lecture given in G\u00f6teborg."},{"key":"S0960129521000268_ref20","doi-asserted-by":"crossref","unstructured":"Hofmann, M. (1994). On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L. and Tiuryn, J. (eds.) CSL, vol. 933. Lecture Notes in Computer Science. Springer.","DOI":"10.1007\/BFb0022273"},{"key":"S0960129521000268_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.10.001"},{"key":"S0960129521000268_ref25","doi-asserted-by":"crossref","unstructured":"Kaposi, A. , Kov\u00e1cs, A. and Altenkirch, T. (2019). Constructing quotient inductive-inductive types. Proceedings of the ACM on Programming Languages, 3 (POPL) 2:1\u20132:24.","DOI":"10.1145\/3290315"},{"key":"S0960129521000268_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"S0960129521000268_ref22","doi-asserted-by":"crossref","unstructured":"Hofmann, M. (1996). Syntax and semantics of dependent types. In: Pitts, A. and Dybjer, P. (eds.) Semantics and Logics of Computation. Cambridge University Press.","DOI":"10.1017\/CBO9780511526619.004"},{"key":"S0960129521000268_ref12","article-title":"Undecidability of equality in the free locally cartesian closed category (extended version)","volume":"13","author":"Castellan","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129521000268_ref21","doi-asserted-by":"crossref","unstructured":"Hofmann, M. (1995). Conservativity of equality reflection over intensional type theory. In: Berardi, S. and Coppo, M. (eds.) Types for Proofs and Programs, International Workshop TYPES 1995, Torino, Italy, June 5\u20138, 1995, Selected Papers, vol. 1158. Lecture Notes in Computer Science. Springer, 153\u2013164.","DOI":"10.1007\/3-540-61780-9_68"},{"key":"S0960129521000268_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"S0960129521000268_ref3","doi-asserted-by":"crossref","unstructured":"Aczel, P. (1998). On relating type theories and set theories. In: Altenkirch, T. , Reus, B. and Naraschewski, W. (eds.) Types for Proofs and Programs. Springer, 33\u201346.","DOI":"10.1007\/3-540-48167-2_1"},{"key":"S0960129521000268_ref33","unstructured":"Voevodsky, V. (2014). Subsystems and regular quotients of C-systems. ArXiv, abs\/1406.7413."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,21]],"date-time":"2022-06-21T05:55:35Z","timestamp":1655790935000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000268\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10]]},"references-count":34,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["S0960129521000268"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000268","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}