{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:22:05Z","timestamp":1760080925101,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":141,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"US Army Research Office","award":["W911NF-20-1-0082"],"award-info":[{"award-number":["W911NF-20-1-0082"]}]},{"name":"US National Science Foundation","award":["DMS-2204304"],"award-info":[{"award-number":["DMS-2204304"]}]},{"name":"US Air Force Office of Scientific Research","award":["FA9550-21-1-0009"],"award-info":[{"award-number":["FA9550-21-1-0009"]}]},{"name":"Simons Fellowship","award":["920415"],"award-info":[{"award-number":["920415"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,1,9]]},"DOI":"10.1145\/3636501.3636945","type":"proceedings-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T19:39:27Z","timestamp":1704829167000},"page":"274-290","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalizing the \u221e-Categorical Yoneda Lemma"],"prefix":"10.1145","author":[{"given":"Nikolai","family":"Kudasov","sequence":"first","affiliation":[{"name":"Innopolis University, Innopolis, Russia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emily","family":"Riehl","sequence":"additional","affiliation":[{"name":"Johns Hopkins University, Baltimore, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Weinberger","sequence":"additional","affiliation":[{"name":"Johns Hopkins University, Baltimore, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Daniel Gratzer, and Lars Birkedal.","author":"Aagaard Frederik Lerbjerg","year":"2022","unstructured":"Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, and Lars Birkedal. 2022. Unifying cubical and multimodal type theory. arxiv:2203.13000."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000486"},{"key":"e_1_3_2_1_3_1","volume-title":"24th International Conference on Types for Proofs and Programs, 11\u201312","author":"Ahrens Benedikt","year":"2018","unstructured":"Benedikt Ahrens and Marco Maggesi. 2018. A modular formalization of bicategories in type theory. 24th International Conference on Types for Proofs and Programs, 11\u201312."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533334"},{"key":"e_1_3_2_1_5_1","volume-title":"Paige Randall North, and Niels Van Der Weide","author":"Ahrens Benedikt","year":"2023","unstructured":"Benedikt Ahrens, Paige Randall North, and Niels Van Der Weide. 2023. Bicategorical type theory: semantics and syntax. Mathematical Structures in Computer Science, 1\u201345."},{"key":"e_1_3_2_1_6_1","unstructured":"Antoine Allioux Eric Finster and Matthieu Sozeau. 2021. Types are Internal \u221e -Groupoids. arxiv:2105.00024."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Danil Annenkov Paolo Capriotti Nicolai Kraus and Christian Sattler. 2023. Two-level type theory and applications. Mathematical Structures in Computer Science may 1\u201356. https:\/\/doi.org\/10.1017\/s0960129523000130 10.1017\/s0960129523000130","DOI":"10.1017\/s0960129523000130"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2018.08.002"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2020.05"},{"key":"e_1_3_2_1_12_1","unstructured":"David Ayala Aaron Mazel-Gee and Nick Rozenblyum. 2022. Stratified noncommutative geometry. arxiv:1910.14602."},{"key":"e_1_3_2_1_13_1","unstructured":"Fredrik Bakke. 2021. Segal Spaces in Homotopy Type Theory. Master\u2019s thesis. NTNU. https:\/\/ntnuopen.ntnu.no\/ntnu-xmlui\/handle\/11250\/2995704"},{"key":"e_1_3_2_1_14_1","unstructured":"C\u00e9sar Bardomiano Mart\u00ednez. 2022. Limits and exponentiable functors in simplicial homotopy type theory. arxiv:2202.12386."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Clark Barwick and Jay Shah. 2018. Fibrations in \u221e -category theory. 2016 MATRIX annals 17\u201342. https:\/\/www.matrix-inst.org.au\/wp_Matrix2016\/wp-content\/uploads\/2017\/08\/BarwickShah.pdf","DOI":"10.1007\/978-3-319-72299-3_2"},{"key":"e_1_3_2_1_16_1","unstructured":"Thibaut Benjamin Eric Finster and Samuel Mimram. 2021. Globular weak omega-categories as models of a type theory. arXiv:2106.04475."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781316181874"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2013.107"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.2140\/gt.2013.17.733"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0068547"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575679"},{"key":"e_1_3_2_1_23_1","unstructured":"Aldridge K. Bousfield. 1992. The simplicial homotopy theory of iterated loop spaces. Typed notes by Julie Bergner"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-15655-8_7"},{"volume-title":"Type-theoretic Modalities for Synthetic (\u221e ,1)-Categories. https:\/\/hott.github.io\/HoTT-2019\/\/conf-slides\/Weinberger.pdf Talk at HoTT 2019 Conference at CMU","author":"Buchholtz Ulrik","key":"e_1_3_2_1_27_1","unstructured":"Ulrik Buchholtz and Jonathan Weinberger. 2019. Type-theoretic Modalities for Synthetic (\u221e ,1)-Categories. https:\/\/hott.github.io\/HoTT-2019\/\/conf-slides\/Weinberger.pdf Talk at HoTT 2019 Conference at CMU, Pittsburgh, CA"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2023.04"},{"key":"e_1_3_2_1_29_1","volume-title":"A whirlwind tour of the world of (\u221e , 1)-categories. Mexican mathematicians abroad: recent contributions, 657","author":"Camarena Omar Antol\u2208","year":"2013","unstructured":"Omar Antol\u2208 Camarena. 2013. A whirlwind tour of the world of (\u221e , 1)-categories. Mexican mathematicians abroad: recent contributions, 657 (2013), 15\u201361. https:\/\/www.matem.unam.mx\/~omar\/papers\/infinity-survey.pdf"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.14"},{"key":"e_1_3_2_1_31_1","unstructured":"Felix Cherubini. 2022. Cartan Geometry in Modal Homotopy Type Theory. arxiv:1806.05966."},{"volume-title":"Higher categories and homotopical algebra. 180","author":"Cisinski Denis-Charles","key":"e_1_3_2_1_32_1","unstructured":"Denis-Charles Cisinski. 2019. Higher categories and homotopical algebra. 180, Cambridge University Press."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_2_1_34_1","unstructured":"Pedro Boavida de Brito. 2016. Segal objects and the Grothendieck construction. arxiv:1605.00706."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_1_37_1","unstructured":"Christopher J. Dean. 2020. Globular Multicategories with Homomorphism Types. arxiv:2005.14104."},{"key":"e_1_3_2_1_38_1","unstructured":"Eugene W. Stark. 2016. Category Theory with Adjunctions and Limits. Archive of Formal Proofs June issn:2150-914x https:\/\/isa-afp.org\/entries\/Category3.html"},{"key":"e_1_3_2_1_39_1","unstructured":"Laurent Fargues and Peter Scholze. 2021. Geometrization of the local Langlands correspondence. arxiv:2102.13459."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005124"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533363"},{"key":"e_1_3_2_1_42_1","unstructured":"Eric Finster Alex Rice and Jamie Vicary. 2021. A Type Theory for Strictly Associative Infinity Categories. arxiv:2109.01513."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785708"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007646"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2210.05420"},{"key":"e_1_3_2_1_49_1","unstructured":"Greg O\u2019Keefe. 2005. Category Theory to Yoneda\u2019s Lemma. Archive of Formal Proofs April issn:2150-914x https:\/\/isa-afp.org\/entries\/Category.html"},{"key":"e_1_3_2_1_50_1","unstructured":"Alexander Grothendieck. 1961. Techniques de construction et th\u00e9or\u00e8mes d\u2019existence en g\u00e9om\u00e9trie alg\u00e9brique III : pr\u00e9sch\u00e9mas quotients. In S\u00e9minaire Bourbaki : ann\u00e9es 1960\/61 expos\u00e9s 205-222 (S\u00e9minaire Bourbaki). Soci\u00e9t\u00e9 math\u00e9matique de France. http:\/\/www.numdam.org\/item\/SB_1960-1961__6__99_0\/ talk:212"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00209-014-1390-7"},{"key":"e_1_3_2_1_54_1","unstructured":"Andr\u00e9 Hirschowitz and Carlos Simpson. 2001. Descente pour les n-champs (Descent for n-stacks). arxiv:math\/9807049."},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439922"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(02)00135-4"},{"key":"e_1_3_2_1_58_1","unstructured":"Andr\u00e9 Joyal. 2008. Notes on quasi-categories. preprint https:\/\/www.math.uchicago.edu\/~may\/IMA\/Joyal.pdf"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1090\/conm"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS"},{"key":"e_1_3_2_1_61_1","unstructured":"Alexander Katovsky. 2010. Category Theory. Archive of Formal Proofs June issn:2150-914x https:\/\/isa-afp.org\/entries\/Category2.html"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10688-014-0050-3"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470667"},{"key":"e_1_3_2_1_64_1","unstructured":"Nikolai Kudasov. [n. d.]. Rzk. https:\/\/github.com\/rzk-lang\/rzk An experimental proof assistant based on a type theory for synthetic \u221e -categories"},{"key":"e_1_3_2_1_65_1","volume-title":"Functional Pearl: Dependent type inference via free higher-order unification. arxiv:2204.05653. arxiv:2204.05653","author":"Kudasov Nikolai","year":"2022","unstructured":"Nikolai Kudasov. 2022. Functional Pearl: Dependent type inference via free higher-order unification. arxiv:2204.05653. arxiv:2204.05653"},{"key":"e_1_3_2_1_66_1","volume-title":"SCAN","author":"Kudasov Nikolai","year":"2023","unstructured":"Nikolai Kudasov. 2023. Experimental prover for Tope logic. In SCAN 2023. 37\u201339."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.026"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.22"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.25"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2010-304"},{"key":"e_1_3_2_1_71_1","unstructured":"Jacob Lurie. 2003. On Infinity Topoi. arxiv:math\/0306109."},{"volume-title":"Derived algebraic geometry. Ph. D. Dissertation","author":"Lurie Jacob","key":"e_1_3_2_1_72_1","unstructured":"Jacob Lurie. 2004. Derived algebraic geometry. Ph. D. Dissertation. Massachusetts Institute of Technology. http:\/\/hdl.handle.net\/1721.1\/30144"},{"volume-title":"Higher topos theory","author":"Lurie Jacob","key":"e_1_3_2_1_73_1","unstructured":"Jacob Lurie. 2009. Higher topos theory. Princeton University Press. https:\/\/www.math.ias.edu\/~lurie\/papers\/HTT.pdf"},{"key":"e_1_3_2_1_74_1","unstructured":"Jacob Lurie. 2017. Higher Algebra. https:\/\/www.math.ias.edu\/~lurie\/papers\/HA.pdf"},{"key":"e_1_3_2_1_75_1","unstructured":"Jacob Lurie. 2018. Spectral algebraic geometry. https:\/\/www.math.ias.edu\/~lurie\/papers\/SAG-rootfile.pdf Under construction"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_1_77_1","unstructured":"Louis Martini. 2021. Yoneda\u2019s lemma for internal higher categories. arxiv:2103.17141."},{"key":"e_1_3_2_1_78_1","unstructured":"Louis Martini. 2022. Cocartesian fibrations and straightening internal to an \u221e -topos. arxiv:2204.00295."},{"key":"e_1_3_2_1_79_1","unstructured":"Louis Martini and Sebastian Wolf. 2023. Internal higher topos theory. arxiv:2303.06437."},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028395"},{"key":"e_1_3_2_1_82_1","unstructured":"David Jaz Myers. 2021. Modal Fracture of Higher Groups. arxiv:2106.15390."},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2022.04"},{"key":"e_1_3_2_1_84_1","unstructured":"David Jaz Myers. 2022. Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory. arxiv:2205.15887."},{"key":"e_1_3_2_1_85_1","unstructured":"David Jaz Myers and Mitchell Riley. 2023. Commuting Cohesions. arxiv:2301.13780."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2020.107026"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30829-1_6"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.012"},{"key":"e_1_3_2_1_91_1","unstructured":"Andreas Nuyts. 2015. Towards a directed homotopy type theory based on 4 kinds of variance. Master\u2019s thesis. KU Leuven. https:\/\/people.cs.kuleuven.be\/~dominique.devriese\/ThesisAndreasNuyts.pdf"},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.24"},{"key":"e_1_3_2_1_93_1","unstructured":"R\u00e9gis Pellissier. 2002. Cat\u00e9gories enrichies faibles. Ph. D. Dissertation. Universit\u00e9 Nice Sophia Antipolis. arxiv:math\/0308246."},{"key":"e_1_3_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097438"},{"key":"e_1_3_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/s40062-021-00288-2"},{"key":"e_1_3_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2022.v24.n2.a7"},{"key":"e_1_3_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2023.03"},{"key":"e_1_3_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-023-09734-z"},{"key":"e_1_3_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-00-02653-2"},{"key":"e_1_3_2_1_100_1","unstructured":"Emily Riehl. 2023. Could \u221e -category theory be taught to undergraduates? Notices of the AMS May https:\/\/www.ams.org\/journals\/notices\/202305\/noti2692\/noti2692.html"},{"volume-title":"\u201cA panorama of homotopy theory: a conference in honour of Mike Hopkins","author":"Riehl Emily","key":"e_1_3_2_1_101_1","unstructured":"Emily Riehl. 2023. Homotopy types are homotopy types. https:\/\/emilyriehl.github.io\/files\/hopkins65.pdf Lecture notes for an invited talk to \u201cA panorama of homotopy theory: a conference in honour of Mike Hopkins\u201d, Oxford, UK"},{"key":"e_1_3_2_1_102_1","volume-title":"Luminy","author":"Riehl Emily","year":"2023","unstructured":"Emily Riehl. 2023. On the \u221e -topos semantics of homotopy type theory. arxiv:2212.06937. Lecture notes for a mini-course at CIRM, Luminy, Feb 2022"},{"key":"e_1_3_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_3_2_1_104_1","unstructured":"Emily Riehl and Michael Shulman. 2023. A type theory for synthetic \u221e -categories. arxiv:1705.07442v5."},{"key":"e_1_3_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2016.07.003"},{"key":"e_1_3_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108936880"},{"volume-title":"Introduction to Homotopy Type Theory","author":"Rijke Egbert","key":"e_1_3_2_1_107_1","unstructured":"Egbert Rijke. 2022. Introduction to Homotopy Type Theory. Cambridge University Press. arxiv:2212.11082 forthcoming"},{"key":"e_1_3_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:2)2020"},{"key":"e_1_3_2_1_109_1","volume-title":"Licata","author":"Riley Mitchell","year":"2021","unstructured":"Mitchell Riley, Eric Finster, and Daniel R. Licata. 2021. Synthetic Spectra via a Monadic and Comonadic Modality. arxiv:2102.04099."},{"key":"e_1_3_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2021.1926016"},{"key":"e_1_3_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.158.8"},{"key":"e_1_3_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02684591"},{"key":"e_1_3_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2015.v17.n2.a6"},{"key":"e_1_3_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_3_2_1_115_1","unstructured":"Michael Shulman. 2019. All (\u221e 1)-toposes have strict univalent universes. arxiv:1904.07004."},{"key":"e_1_3_2_1_116_1","unstructured":"Eugene W Stark. 2023. Bicategories. https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Bicategory\/outline.pdf"},{"key":"e_1_3_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2022.v24.n1.a12"},{"key":"e_1_3_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2022.107254"},{"key":"e_1_3_2_1_119_1","unstructured":"Jonathan Sterling. [n. d.]. Towards a geometry for syntax. arXiv:2307.09497. Invited contribution to the proceedings of the Chapman Grothendieck Conference to appear"},{"key":"e_1_3_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6990769"},{"key":"e_1_3_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_3_2_1_122_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_3_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2013.04.001"},{"key":"e_1_3_2_1_124_1","unstructured":"The RedPRL Development Team. 2016\u20132018. The RedPRL Proof Assistant. https:\/\/redprl.org"},{"key":"e_1_3_2_1_125_1","unstructured":"The RedPRL Development Team. 2018. The redtt Proof Assistant. https:\/\/github.com\/RedPRL\/redtt\/"},{"key":"e_1_3_2_1_126_1","unstructured":"The RedPRL Development Team. 2021. The cooltt Proof Assistant. https:\/\/github.com\/RedPRL\/cooltt\/"},{"key":"e_1_3_2_1_127_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_3_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms"},{"key":"e_1_3_2_1_129_1","unstructured":"Niels van der Weide Nima Rasekh Benedikt Ahrens and Paige Randall North. 2023. Univalent Double Categories. arxiv:2310.09220."},{"key":"e_1_3_2_1_130_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"},{"key":"e_1_3_2_1_131_1","unstructured":"Vladimir Voevodsky. 2009. A very short note on homotopy \u03bb -calculus. https:\/\/www.math.ias.edu\/~vladimir\/Site3\/Univalent_Foundations_files\/Hlambda_short_current.pdf"},{"key":"e_1_3_2_1_132_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. Unpublished note https:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/HTS.pdf"},{"key":"e_1_3_2_1_133_1","unstructured":"Vladimir Voevodsky Benedikt Ahrens and Daniel Grayson. [n. d.]. UniMath \u2014 a computer-checked library of univalent mathematics. Available at. http:\/\/unimath.org"},{"volume-title":"Directed Type Theory. https:\/\/www.ias.edu\/video\/univalent\/1213\/0410-MichaelWarren Lecture at IAS","author":"Warren Michael","key":"e_1_3_2_1_134_1","unstructured":"Michael Warren. 2013. Directed Type Theory. https:\/\/www.ias.edu\/video\/univalent\/1213\/0410-MichaelWarren Lecture at IAS, Princeton, NJ"},{"key":"e_1_3_2_1_135_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394794"},{"key":"e_1_3_2_1_136_1","doi-asserted-by":"publisher","unstructured":"Jonathan Weinberger. 2022. A Synthetic Perspective on (\u221e 1)-Category Theory: Fibrational and Semantic Aspects. Ph. D. Dissertation. TU Darmstadt. https:\/\/doi.org\/10.26083\/tuprints-00020716 10.26083\/tuprints-00020716","DOI":"10.26083\/tuprints-00020716"},{"key":"e_1_3_2_1_137_1","unstructured":"Jonathan Weinberger. 2022. Internal sums for synthetic fibered (\u221e 1)-categories. arxiv:2205.00386."},{"key":"e_1_3_2_1_138_1","unstructured":"Jonathan Weinberger. 2022. Strict stability of extension types. arxiv:2203.07194."},{"key":"e_1_3_2_1_139_1","unstructured":"Jonathan Weinberger. 2022. Two-sided cartesian fibrations of synthetic (\u221e 1)-categories. arxiv:2204.00938."},{"key":"e_1_3_2_1_140_1","unstructured":"Jonathan Weinberger Benedikt Ahrens Ulrik Buchholtz and Paige North. 2022. Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability. https:\/\/hott-uf.github.io\/2022\/HoTTUF_2022_paper_6.pdf Workshop on Homotopy Type Theory \/ Univalent Foundations"},{"key":"e_1_3_2_1_141_1","unstructured":"Tesla Zhang. 2023. Three non-cubical applications of extension types. arxiv:2311.05658."}],"event":{"name":"CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"London UK","acronym":"CPP '24"},"container-title":["Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636945","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636501.3636945","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:11Z","timestamp":1750287251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636945"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,9]]},"references-count":141,"alternative-id":["10.1145\/3636501.3636945","10.1145\/3636501"],"URL":"https:\/\/doi.org\/10.1145\/3636501.3636945","relation":{},"subject":[],"published":{"date-parts":[[2024,1,9]]},"assertion":[{"value":"2024-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}