{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:44:10Z","timestamp":1782953050306,"version":"3.54.5"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227294","type":"print"},{"value":"9783032227300","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-22730-0_28","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T16:24:58Z","timestamp":1776270298000},"page":"593-615","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A 2-categorical approach to the semantics of dependent type theory with computation axioms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6495-7405","authenticated-orcid":false,"given":"Matteo","family":"Spadetto","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","unstructured":"Ahrens, B., North, P.R., van\u00a0der Weide, N.: Semantics for two-dimensional type theory. In: Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science. pp. [Article 12], 14. ACM, New York (2022). https:\/\/doi.org\/10.1145\/3531130.3533334, https:\/\/doi.org\/10.1145\/3531130.3533334","DOI":"10.1145\/3531130.3533334"},{"key":"28_CR2","doi-asserted-by":"publisher","unstructured":"Ahrens, B., North, P.R., van\u00a0der Weide, N.: Bicategorical type theory: semantics and syntax. Math. Structures Comput. Sci. 33(10), 868\u2013912 (2023). https:\/\/doi.org\/10.1017\/s0960129523000312, https:\/\/doi.org\/10.1017\/s0960129523000312","DOI":"10.1017\/s0960129523000312"},{"key":"28_CR3","unstructured":"Altenkirch, T., Neumann, J.: Synthetic 1-categories in directed type theory. arXiv:2410.19520"},{"key":"28_CR4","doi-asserted-by":"publisher","unstructured":"Arndt, P., Kapulkin, K.: Homotopy-theoretic models of type theory. In: Typed lambda calculi and applications. 10th international conference, TLCA 2011, Novi Sad, Serbia, June 1\u20133, 2011. Proceedings, pp. 45\u201360. Berlin: Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21691-6_7","DOI":"10.1007\/978-3-642-21691-6_7"},{"key":"28_CR5","doi-asserted-by":"publisher","unstructured":"Awodey, S.: Natural models of homotopy type theory. Math. Structures Comput. Sci. 28(2), 241\u2013286 (2018). https:\/\/doi.org\/10.1017\/S0960129516000268, https:\/\/doi.org\/10.1017\/S0960129516000268","DOI":"10.1017\/S0960129516000268"},{"key":"28_CR6","doi-asserted-by":"publisher","unstructured":"Awodey, S., Gambino, N., Sojakova, K.: Inductive types in homotopy type theory. In: Proceedings of the 2012 27th Annual ACM\/IEEE Symposium on Logic in Computer Science. pp. 95\u2013104. IEEE Computer Soc., Los Alamitos, CA (2012). https:\/\/doi.org\/10.1109\/LICS.2012.21, https:\/\/doi.org\/10.1109\/LICS.2012.21","DOI":"10.1109\/LICS.2012.21"},{"key":"28_CR7","doi-asserted-by":"publisher","unstructured":"Awodey, S., Gambino, N., Sojakova, K.: Homotopy-initial algebras in type theory. J. ACM 63(6), Art. 51, 45 (2017). https:\/\/doi.org\/10.1145\/3006383, https:\/\/doi.org\/10.1145\/3006383","DOI":"10.1145\/3006383"},{"key":"28_CR8","doi-asserted-by":"publisher","unstructured":"Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Cambridge Philos. Soc. 146(1), 45\u201355 (2009). https:\/\/doi.org\/10.1017\/S0305004108001783, https:\/\/doi.org\/10.1017\/S0305004108001783","DOI":"10.1017\/S0305004108001783"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"van\u00a0den Berg, B.: Path categories and propositional identity types. ACM Trans. Comput. Log. 19(2), Art. 15, 32 (2018). https:\/\/doi.org\/10.1145\/3204492, https:\/\/doi.org\/10.1145\/3204492","DOI":"10.1145\/3204492"},{"key":"28_CR10","unstructured":"van\u00a0den Berg, B., den Besten, M.: Quadratic type checking for objective type theory. http:\/\/arxiv.org\/abs\/2102.00905arXiv:2102.00905 (2021)"},{"key":"28_CR11","doi-asserted-by":"publisher","unstructured":"van\u00a0den Berg, B., Moerdijk, I.: Exact completion of path categories and algebraic set theory. Part I: Exact completion of path categories. J. Pure Appl. Algebra 222(10), 3137\u20133181 (2018). https:\/\/doi.org\/10.1016\/j.jpaa.2017.11.017, https:\/\/doi.org\/10.1016\/j.jpaa.2017.11.017","DOI":"10.1016\/j.jpaa.2017.11.017"},{"key":"28_CR12","unstructured":"Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: 19th International Conference on Types for Proofs and Programs, LIPIcs. Leibniz Int. Proc. Inform., vol.\u00a026, pp. 107\u2013128. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern (2014)"},{"key":"28_CR13","unstructured":"Bocquet, R.: Coherence of strict equalities in dependent type theories. http:\/\/arxiv.org\/abs\/2010.14166arXiv:2010.14166 (2020)"},{"key":"28_CR14","doi-asserted-by":"publisher","unstructured":"Bocquet, R.: Strictification of weakly stable type-theoretic structures using generic contexts. In: 27th International Conference on Types for Proofs and Programs, LIPIcs. Leibniz Int. Proc. Inform., vol.\u00a0239, pp. Art. No. 3, 23. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern (2022). https:\/\/doi.org\/10.4230\/lipics.types.2021.3, https:\/\/doi.org\/10.4230\/lipics.types.2021.3","DOI":"10.4230\/lipics.types.2021.3"},{"key":"28_CR15","unstructured":"Boulier, S., Winterhalter, T.: Weak type theory is rather strong. 30th International Conference on Types for Proofs and Programs (2019), https:\/\/www.ii.uib.no\/~bezem\/abstracts\/TYPES_2019_paper_18"},{"key":"28_CR16","unstructured":"Cartmell, J.: Generalised Algebraic Theories and Contextual Categories. Ph.D. thesis, University of Oxford (1978)"},{"key":"28_CR17","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, https:\/\/doi.org\/10.1017\/S0960129513000881","DOI":"10.1017\/S0960129513000881"},{"key":"28_CR18","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. In: 21st International Conference on Types for Proofs and Programs, LIPIcs, vol.\u00a069 (2018)"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"Coquand, T., Danielsson, N.A.: Isomorphism is equality. Indag. Math. (N.S.) 24(4), 1105\u20131120 (2013). https:\/\/doi.org\/10.1016\/j.indag.2013.09.002, https:\/\/doi.org\/10.1016\/j.indag.2013.09.002","DOI":"10.1016\/j.indag.2013.09.002"},{"key":"28_CR20","doi-asserted-by":"publisher","unstructured":"Curien, P.L., Garner, R., Hofmann, M.: Revisiting the categorical interpretation of dependent type theory. Theoret. Comput. Sci. 546, 99\u2013119 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.03.003, https:\/\/doi.org\/10.1016\/j.tcs.2014.03.003","DOI":"10.1016\/j.tcs.2014.03.003"},{"key":"28_CR21","unstructured":"Dybjer, P.: Internal type theory. In: Types for Proofs and Programs: International Workshop, TYPES\u201995, Torino, Italy, June 5-8, 1995 Selected Papers. vol.\u00a01158, p.\u00a0120. Springer Science & Business Media (1996)"},{"key":"28_CR22","doi-asserted-by":"publisher","unstructured":"Fiore, M., Saville, P.: A type theory for Cartesian closed bicategories. In: Proceedings of the 2019 34th annual ACM\/IEEE symposium on logic in computer science, LICS 2019, Vancouver, Canada, June 24\u201327, 2019, p.\u00a013. Piscataway, NJ: IEEE Press (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785708, https:\/\/dl.acm.org\/doi\/10.5555\/3470152.3470190, id\/No 38","DOI":"10.1109\/LICS.2019.8785708"},{"key":"28_CR23","doi-asserted-by":"publisher","unstructured":"Gambino, N., Garner, R.: The identity type weak factorisation system. Theoretical Computer Science 409(1), 94\u2013109 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2008.08.030, http:\/\/dx.doi.org\/10.1016\/j.tcs.2008.08.030","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"28_CR24","doi-asserted-by":"publisher","unstructured":"Garner, R.: Two-dimensional models of type theory. Math. Structures Comput. Sci. 19(4), 687\u2013736 (2009). https:\/\/doi.org\/10.1017\/S0960129509007646, https:\/\/doi.org\/10.1017\/S0960129509007646","DOI":"10.1017\/S0960129509007646"},{"key":"28_CR25","unstructured":"Hofmann, M.: Extensional concepts in intensional type theory. Ph.D. thesis, University of Edinburgh (1995)"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) Computer Science Logic. pp. 427\u2013441. Springer Berlin Heidelberg, Berlin, Heidelberg (1995)","DOI":"10.1007\/BFb0022273"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Conservativity of equality reflection over intensional type theory. In: Berardi, S., Coppo, M. (eds.) Types for Proofs and Programs. pp. 153\u2013164. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)","DOI":"10.1007\/3-540-61780-9_68"},{"key":"28_CR28","doi-asserted-by":"publisher","unstructured":"Hofmann, M.: Syntax and semantics of dependent types, pp. 13\u201354. Springer, London (1997). https:\/\/doi.org\/10.1007\/978-1-4471-0963-1_2, https:\/\/doi.org\/10.1007\/978-1-4471-0963-1_2","DOI":"10.1007\/978-1-4471-0963-1_2"},{"key":"28_CR29","unstructured":"Hofmann, M., Streicher, T.: The groupoid model refutes uniqueness of identity proofs. In: Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994). pp. 208\u2013212. IEEE Computer Society Press (July 1994)"},{"key":"28_CR30","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-five years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol.\u00a036, pp. 83\u2013111. Oxford Univ. Press, New York (1998)","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"28_CR31","doi-asserted-by":"publisher","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, https:\/\/doi.org\/10.1016\/0304-3975(93)90169-T","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"28_CR32","unstructured":"Jacobs, B.: Categorical logic and type theory, Studies in Logic and the Foundations of Mathematics, vol.\u00a0141. North-Holland Publishing Co., Amsterdam (1999)"},{"key":"28_CR33","doi-asserted-by":"publisher","unstructured":"Kapulkin, K., Lumsdaine, P.L.: Homotopical inverse diagrams in categories with attributes. Journal of Pure and Applied Algebra 225(4), 106563 (2021). https:\/\/doi.org\/10.1016\/j.jpaa.2020.106563, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0022404920302644","DOI":"10.1016\/j.jpaa.2020.106563"},{"key":"28_CR34","doi-asserted-by":"publisher","unstructured":"Kapulkin, K., Lumsdaine, P.L.: The homotopy theory of type theories. Adv. Math. 337, 1\u201338 (2018). https:\/\/doi.org\/10.1016\/j.aim.2018.08.003","DOI":"10.1016\/j.aim.2018.08.003"},{"key":"28_CR35","doi-asserted-by":"publisher","unstructured":"Laretto, A., Loregian, F., Veltri, N.: Di- is for directed: First-order directed type theory via dinaturality. Proc. ACM Program. Lang. 10(POPL) (Jan 2026). https:\/\/doi.org\/10.1145\/3776703, https:\/\/doi.org\/10.1145\/3776703","DOI":"10.1145\/3776703"},{"key":"28_CR36","doi-asserted-by":"publisher","unstructured":"Lumsdaine, P.L., Warren, M.A.: The local universes model: an overlooked coherence construction for dependent type theories. ACM Trans. Comput. Log. 16(3), Art. 23, 31 (2015). https:\/\/doi.org\/10.1145\/2754931, https:\/\/doi.org\/10.1145\/2754931","DOI":"10.1145\/2754931"},{"key":"28_CR37","doi-asserted-by":"publisher","unstructured":"Maietti, M.E.: Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Structures Comput. Sci. 15(6), 1089\u20131149 (2005). https:\/\/doi.org\/10.1017\/S0960129505004962, https:\/\/doi.org\/10.1017\/S0960129505004962","DOI":"10.1017\/S0960129505004962"},{"key":"28_CR38","doi-asserted-by":"publisher","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, https:\/\/doi.org\/10.1017\/S0960129500000074","DOI":"10.1017\/S0960129500000074"},{"key":"28_CR39","doi-asserted-by":"crossref","unstructured":"Moss, S.K., von Glehn, T.: Dialectica models of type theory. In: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. p. 739\u2013748. Association for Computing Machinery, New York, NY, USA (2018)","DOI":"10.1145\/3209108.3209207"},{"key":"28_CR40","doi-asserted-by":"publisher","unstructured":"North, P.R.: Towards a directed homotopy type theory. In: Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics. Electron. Notes Theor. Comput. Sci., vol.\u00a0347, pp. 223\u2013239. Elsevier Sci. B. V., Amsterdam (2019). https:\/\/doi.org\/10.1016\/j.entcs.2019.09.012, https:\/\/doi.org\/10.1016\/j.entcs.2019.09.012","DOI":"10.1016\/j.entcs.2019.09.012"},{"key":"28_CR41","unstructured":"Otten, D., Spadetto, M.: The biequivalence of path categories and axiomatic Martin-L\u00f6f type theories. In: 34rd EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs) (2026). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CSL.2026.38 (full version)"},{"key":"28_CR42","doi-asserted-by":"publisher","unstructured":"Paulson, L.C.: Formalising mathematics in simple type theory. In: Reflections on the foundations of mathematics\u2014univalent foundations, set theory and general thoughts, Synth. Libr., vol.\u00a0407, pp. 437\u2013453. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-15655-8_20, https:\/\/doi.org\/10.1007\/978-3-030-15655-8_20","DOI":"10.1007\/978-3-030-15655-8_20"},{"key":"28_CR43","doi-asserted-by":"publisher","unstructured":"Riehl, E.: Categorical homotopy theory, New Math. Monogr., vol.\u00a024. Cambridge: Cambridge University Press (2014). https:\/\/doi.org\/10.1017\/CBO9781107261457","DOI":"10.1017\/CBO9781107261457"},{"key":"28_CR44","doi-asserted-by":"publisher","unstructured":"Seely, R.A.G.: Locally Cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95(1), 33\u201348 (1984). https:\/\/doi.org\/10.1017\/S0305004100061284, https:\/\/doi.org\/10.1017\/S0305004100061284","DOI":"10.1017\/S0305004100061284"},{"key":"28_CR45","unstructured":"Spadetto, M.: A 2-categorical approach to the semantics of dependent type theory with computation axioms (extended version). http:\/\/arxiv.org\/abs\/2507.07208arXiv:2507.07208 (2025)"},{"key":"28_CR46","doi-asserted-by":"publisher","unstructured":"Spadetto, M.: Relating homotopy equivalences to conservativity in dependent type theories with computation axioms. Logical Methods in Computer Science Volume 21, Issue 3, 32 (Sep 2025). https:\/\/doi.org\/10.46298\/lmcs-21(3:32)2025, https:\/\/lmcs.episciences.org\/11565","DOI":"10.46298\/lmcs-21(3:32)2025"},{"key":"28_CR47","doi-asserted-by":"publisher","unstructured":"Streicher, T.: Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions, pp. 156\u2013220. Birkh\u00e4user Boston, Boston, MA (1991). https:\/\/doi.org\/10.1007\/978-1-4612-0433-6_4, https:\/\/doi.org\/10.1007\/978-1-4612-0433-6_4","DOI":"10.1007\/978-1-4612-0433-6_4"},{"key":"28_CR48","doi-asserted-by":"publisher","unstructured":"Streicher, T.: Semantics of type theory \u2014 Correctness, completeness and independence results. Progress in Theoretical Computer Science, Birkh\u00e4user Boston, Inc., Boston, MA (1991). https:\/\/doi.org\/10.1007\/978-1-4612-0433-6, https:\/\/doi.org\/10.1007\/978-1-4612-0433-6","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"28_CR49","doi-asserted-by":"publisher","unstructured":"Streicher, T.: The genesis of the groupoid model. Math. Structures Comput. Sci. 31(9), 1003\u20131005 (2021). https:\/\/doi.org\/10.1017\/S0960129520000286, https:\/\/doi.org\/10.1017\/S0960129520000286","DOI":"10.1017\/S0960129520000286"},{"key":"28_CR50","unstructured":"Taylor, P.: Practical foundations of mathematics, Cambridge Studies in Advanced Mathematics, vol.\u00a059. Cambridge University Press (1999)"},{"key":"28_CR51","unstructured":"Univalent Foundations Program, T.: Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study (2013)"},{"key":"28_CR52","unstructured":"Vidmar, J.: Polynomial functors and W-types for groupoids. Ph.D. thesis, University of Leeds (2018), https:\/\/etheses.whiterose.ac.uk\/22517\/"},{"key":"28_CR53","unstructured":"Winterhalter, T.: Formalisation and meta-theory of type theory. Ph.D. thesis, Universit\u00e9 de Nantes (2020)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22730-0_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T23:48:26Z","timestamp":1782949706000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22730-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227294","9783032227300"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22730-0_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author has no competing interests to declare that\u00a0are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2026\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}