{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:26Z","timestamp":1767929546550,"version":"3.49.0"},"publisher-location":"Singapore","reference-count":43,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819789429","type":"print"},{"value":"9789819789436","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-97-8943-6_1","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"3-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Comparing Semantic Frameworks for\u00a0Dependently-Sorted Algebraic Theories"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6786-4538","authenticated-orcid":false,"given":"Benedikt","family":"Ahrens","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1390-2970","authenticated-orcid":false,"given":"Peter LeFanu","family":"Lumsdaine","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7876-0956","authenticated-orcid":false,"given":"Paige Randall","family":"North","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"issue":"3","key":"1_CR1","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s000120050111","volume":"41","author":"J Ad\u00e1mek","year":"1999","unstructured":"Ad\u00e1mek, J., H\u00e9bert, M., Rosick\u00fd, J.: On essentially algebraic theories and their generalizations. Algebra Universalis 41(3), 213\u2013227 (1999). https:\/\/doi.org\/10.1007\/s000120050111","journal-title":"Algebra Universalis"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Ad\u00e1mek, J., Rosick\u00fd, J.: Locally presentable and accessible categories, London Mathematical Society Lecture Note Series, vol.\u00a0189. Cambridge University Press, Cambridge (1994). https:\/\/doi.org\/10.1017\/CBO9780511600579","DOI":"10.1017\/CBO9780511600579"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Ahrens, B., Emmenegger, J., North, P.R., Rijke, E.: B-systems and C-systems are equivalent. The Journal of Symbolic Logic p. 1-9 (2023). https:\/\/doi.org\/10.1017\/jsl.2023.41","DOI":"10.1017\/jsl.2023.41"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Ahrens, B., Lumsdaine, P.L., Voevodsky, V.: Categorical structures for type theory in univalent foundations. Logical Methods in Computer Science 14(3), 1\u201318 (9 2018). https:\/\/doi.org\/10.23638\/LMCS-14(3:18)2018","DOI":"10.23638\/LMCS-14(3:18)2018"},{"issue":"2","key":"1_CR5","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1017\/S0960129516000268","volume":"28","author":"S Awodey","year":"2018","unstructured":"Awodey, S.: Natural models of homotopy type theory. Math. Struct. Comput. Sci. 28(2), 241\u2013286 (2018). https:\/\/doi.org\/10.1017\/S0960129516000268","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"1_CR6","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0305004108001783","volume":"146","author":"S Awodey","year":"2009","unstructured":"Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Cam. Phil. Soc. 146(1), 45\u201355 (2009). https:\/\/doi.org\/10.1017\/S0305004108001783","journal-title":"Math. Proc. Cam. Phil. Soc."},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"van\u00a0den Berg, B., Garner, R.: Topological and simplicial models of identity types. ACM Trans. Comput. Log. 13(1), Art. 3, 44 (2012). https:\/\/doi.org\/10.1145\/2071368.2071371","DOI":"10.1145\/2071368.2071371"},{"issue":"2","key":"1_CR8","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1017\/s0960129519000197","volume":"30","author":"L Birkedal","year":"2020","unstructured":"Birkedal, L., Clouston, R., Mannaa, B., M\u00f8gelberg, R.E., Pitts, A.M., Spitters, B.: Modal dependent type theory and dependent right adjoints. Math. Structures Comput. Sci. 30(2), 118\u2013138 (2020). https:\/\/doi.org\/10.1017\/s0960129519000197","journal-title":"Math. Structures Comput. Sci."},{"key":"1_CR9","unstructured":"Blanco, J.: Relating categorical approaches to type dependency (1991), masters thesis, Univ.\u00a0Nijmegen"},{"key":"1_CR10","unstructured":"de\u00a0Boer, M.: A proof and formalization of the initiality conjecture of dependent type theory (2020), http:\/\/www.diva-portal.org\/smash\/record.jsf?pid=diva2%3A1431287 licentiate thesis, Stockholm University"},{"key":"1_CR11","unstructured":"Cartmell, J.: Generalised algebraic theories and contextual categories. Ph.D. thesis, Oxford (1978)"},{"issue":"3","key":"1_CR12","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J Cartmell","year":"1986","unstructured":"Cartmell, J.: Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic 32(3), 209\u2013243 (1986)","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Clairambault, P., Dybjer, P.: The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Math. Structures Comput. Sci. 24(6), e240606, 54 (2014). https:\/\/doi.org\/10.1017\/S0960129513000881","DOI":"10.1017\/S0960129513000881"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/J.TCS.2014.03.003","volume":"546","author":"P Curien","year":"2014","unstructured":"Curien, P., Garner, R., Hofmann, M.: Revisiting the categorical interpretation of dependent type theory. Theor. Comput. Sci. 546, 99\u2013119 (2014). https:\/\/doi.org\/10.1016\/J.TCS.2014.03.003","journal-title":"Theor. Comput. Sci."},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) Types for proofs and programs (Torino, 1995). Lecture Notes in Comput. Sci., vol.\u00a01158, pp. 120\u2013134. Springer, Berlin (1996). https:\/\/doi.org\/10.1007\/3-540-61780-9_66","DOI":"10.1007\/3-540-61780-9_66"},{"key":"1_CR16","unstructured":"Fiore, M.: Discrete generalised polynomial functors (2012), http:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/ICALP2012.pdf, slides from talk given at ICALP 2012"},{"issue":"1","key":"1_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0004972700044828","volume":"7","author":"P Freyd","year":"1972","unstructured":"Freyd, P.: Aspects of topoi. Bull. Aust. Math. Soc. 7(1), 1\u201376 (1972). https:\/\/doi.org\/10.1017\/S0004972700044828","journal-title":"Bull. Aust. Math. Soc."},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Gabriel, P., Ulmer, F.: Lokal pr\u00e4sentierbare Kategorien. Lecture Notes in Mathematics, vol. 221. Springer-Verlag, Berlin-New York (1971). https:\/\/doi.org\/10.1007\/BFb0059396","DOI":"10.1007\/BFb0059396"},{"issue":"6","key":"1_CR19","doi-asserted-by":"publisher","first-page":"1885","DOI":"10.1016\/j.jpaa.2014.07.015","volume":"219","author":"R Garner","year":"2015","unstructured":"Garner, R.: Combinatorial structure of type dependency. J. Pure Appl. Algebra 219(6), 1885\u20131914 (2015). https:\/\/doi.org\/10.1016\/j.jpaa.2014.07.015","journal-title":"J. Pure Appl. Algebra"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Hofmann, M.: On the interpretation of type theory in locally Cartesian closed categories. In: Computer science logic (Kazimierz, 1994), Lecture Notes in Comput. Sci., vol.\u00a0933, pp. 427\u2013441. Springer, Berlin (1995). https:\/\/doi.org\/10.1007\/BFb0022273","DOI":"10.1007\/BFb0022273"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Semantics and logics of computation (Cambridge, 1995), Publ. Newton Inst., vol.\u00a014, pp. 79\u2013130. Cambridge Univ. Press, Cambridge (1997). https:\/\/doi.org\/10.1017\/CBO9780511526619.004","DOI":"10.1017\/CBO9780511526619.004"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Hyland, J.M.E., Pitts, A.M.: The theory of constructions: categorical semantics and topos-theoretic models. In: Categories in computer science and logic (Boulder, CO, 1987), Contemp. Math., vol.\u00a092, pp. 137\u2013199. Amer. Math. Soc., Providence, RI (1989). https:\/\/doi.org\/10.1090\/conm\/092\/1003199","DOI":"10.1090\/conm\/092\/1003199"},{"issue":"2","key":"1_CR23","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(93)90169-T","volume":"107","author":"B Jacobs","year":"1993","unstructured":"Jacobs, B.: Comprehension categories and the semantics of type dependency. Theoret. Comput. Sci. 107(2), 169\u2013207 (1993). https:\/\/doi.org\/10.1016\/0304-3975(93)90169-T","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Johnstone, P.T.: Sketches of an elephant: a topos theory compendium, Oxford Logic Guides, vol. 43,44. The Clarendon Press Oxford University Press, New York (2002)","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"1_CR25","unstructured":"Joyal, A.: Notes on clans and tribes (2017), https:\/\/arxiv.org\/abs\/1710.10238, unpublished notes"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Kapulkin, K., Lumsdaine, P.L.: Homotopical inverse diagrams in categories with attributes. J. Pure Appl. Algebra 225(4), Paper No. 106563, 44 (2021). https:\/\/doi.org\/10.1016\/j.jpaa.2020.106563","DOI":"10.1016\/j.jpaa.2020.106563"},{"issue":"1","key":"1_CR27","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0004972700005591","volume":"26","author":"GM Kelly","year":"1982","unstructured":"Kelly, G.M.: On the essentially-algebraic theory generated by a sketch. Bull. Austral. Math. Soc. 26(1), 45\u201356 (1982). https:\/\/doi.org\/10.1017\/S0004972700005591","journal-title":"Bull. Austral. Math. Soc."},{"issue":"12","key":"1_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2022.107126","volume":"226","author":"F Lucatelli Nunes","year":"2022","unstructured":"Lucatelli Nunes, F., Sousa, L.: On lax epimorphisms and the associated factorization. J. Pure Appl. Algebra 226(12), 107126 (2022). https:\/\/doi.org\/10.1016\/j.jpaa.2022.107126. https:\/\/www.sciencedirect.com\/science\/article\/pii\/ S0022404922001220","journal-title":"J. Pure Appl. Algebra"},{"key":"1_CR29","unstructured":"Makkai, M.: First order logic with dependent sorts, with applications to category theory (1995), http:\/\/www.math.mcgill.ca\/makkai\/folds\/foldsinpdf\/FOLDS.pdf"},{"key":"1_CR30","unstructured":"Martin-L\u00f6f, P.: Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, vol.\u00a01. Bibliopolis, Naples (1984)"},{"issue":"1","key":"1_CR31","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1017\/S0960129500000074","volume":"1","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: A category-theoretic account of program modules. Math. Structures Comput. Sci. 1(1), 103\u2013139 (1991). https:\/\/doi.org\/10.1017\/S0960129500000074","journal-title":"Math. Structures Comput. Sci."},{"key":"1_CR32","unstructured":"Newstead, C.: Algebraic models of dependent type theory. Ph.D. thesis, Carnegie Mellon University (2018), https:\/\/arxiv.org\/abs\/2103.06155"},{"issue":"3","key":"1_CR33","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1016\/j.apal.2006.10.001","volume":"145","author":"E Palmgren","year":"2007","unstructured":"Palmgren, E., Vickers, S.J.: Partial horn logic and Cartesian categories. Ann. Pure Appl. Logic 145(3), 314\u2013353 (2007). https:\/\/doi.org\/10.1016\/j.apal.2006.10.001","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Categorical logic. In: Handbook of Logic in Computer Science, vol.\u00a05, pp. 39\u2013128. Oxford Univ. Press, New York (2000). https:\/\/doi.org\/10.1093\/oso\/9780198537816.001.0001","DOI":"10.1093\/oso\/9780198537816.001.0001"},{"key":"1_CR35","unstructured":"Power, J.: 2-categories. Tech. Rep. NS-98-7, Basic Research in Computer Science, Aarhus (Aug 1998), https:\/\/www.brics.dk\/NS\/98\/7\/index.html"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Streicher, T.: Semantics of type theory: Correctness, completeness, and independence results. Progress in Theoretical Computer Science, Birkh\u00e4user, Boston, MA (1991). https:\/\/doi.org\/10.1007\/978-1-4612-0433-6","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Subramaniam, C.L.: From dependent type theory to higher algebraic structures. Ph.D. thesis, Universit\u00e9 Paris Diderot (2021). https:\/\/doi.org\/10.48550\/arXiv.2110.02804","DOI":"10.48550\/arXiv.2110.02804"},{"key":"1_CR38","unstructured":"Taylor, P.: Recursive Domains, Indexed Category Theory and Polymorphism. Ph.D. thesis, University of Cambridge (1986), https:\/\/www.paultaylor.eu\/domains\/recdic.pdf"},{"key":"1_CR39","unstructured":"Taylor, P.: Practical foundations of mathematics, Cambridge Studies in Advanced Mathematics, vol.\u00a059. Cambridge University Press, Cambridge (1999), https:\/\/www.paultaylor.eu\/~pt\/prafm\/"},{"issue":"3","key":"1_CR40","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1017\/S0960129523000208","volume":"33","author":"T Uemura","year":"2023","unstructured":"Uemura, T.: A general framework for the semantics of type theory. Math. Struct. Comput. Sci. 33(3), 134\u2013179 (2023). https:\/\/doi.org\/10.1017\/S0960129523000208","journal-title":"Math. Struct. Comput. Sci."},{"key":"1_CR41","unstructured":"Voevodsky, V.: B-systems (2016), https:\/\/www.math.ias.edu\/Voevodsky\/files\/files-annotated\/Dropbox\/Unfinished_papers\/Type_systems\/Notes_on_Type_Systems\/Bsystems\/B_systems_current.pdf, unpublished manuscript, revision of arXiv:1410.5389"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Voevodsky, V.: Subsystems and regular quotients of C-systems. In: A panorama of mathematics: pure and applied, Contemp. Math., vol.\u00a0658, pp. 127\u2013137. Amer. Math. Soc., Providence, RI (2016). https:\/\/doi.org\/10.1090\/conm\/658\/13124","DOI":"10.1090\/conm\/658\/13124"},{"issue":"6","key":"1_CR43","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2022.107283","volume":"227","author":"V Voevodsky","year":"2023","unstructured":"Voevodsky, V.: C-system of a module over a $${Jf}$$-relative monad. J. Pure Appl. Algebra 227(6), 107283 (2023). https:\/\/doi.org\/10.1016\/j.jpaa.2022.107283","journal-title":"J. Pure Appl. Algebra"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-97-8943-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:37Z","timestamp":1748364757000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}