More Web Proxy on the site http://driver.im/

research-article

Open access

Semantics for two-dimensional type theory

Authors:

Benedikt Ahrens,

Paige Randall North,

Niels van der WeideAuthors Info & Claims

LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

Article No.: 12, Pages 1 - 14

https://doi.org/10.1145/3531130.3533334

Published: 04 August 2022 Publication History

All formats PDF

Abstract

We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature.

From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory.

The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.

This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.

References

[1]

Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide. 2019. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131), Herman Geuvers (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 5:1–5:17. https://doi.org/10.4230/LIPIcs.FSCD.2019.5

[2]

Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. 2022. Bicategories in univalent foundations. Mathematical Structures in Computer Science(2022), 1–38. https://doi.org/10.1017/S0960129522000032

[3]

Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. 2015. Univalent categories and the Rezk completion. Math. Struct. Comput. Sci. 25, 5 (2015), 1010–1039. https://doi.org/10.1017/S0960129514000486

[4]

Benedikt Ahrens and Peter LeFanu Lumsdaine. 2019. Displayed Categories. Log. Methods Comput. Sci. 15, 1 (2019). https://doi.org/10.23638/LMCS-15(1:20)2019

[5]

Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. 2018. Globular: an online proof assistant for higher-dimensional rewriting. Log. Methods Comput. Sci. 14, 1 (2018). https://doi.org/10.23638/LMCS-14(1:8)2018

[6]

Jean Bénabou. 1967. Introduction to bicategories. In Reports of the Midwest Category Seminar. Springer Berlin Heidelberg, Berlin, Heidelberg, 1–77. https://doi.org/10.1007/BFb0074299

[7]

Thibaut Benjamin, Eric Finster, and Samuel Mimram. 2021. Globular weak ω-categories as models of a type theory. CoRR (2021). arXiv:2106.04475

[8]

Benno van den Berg and Richard Garner. 2011. Types are weak ω-groupoids. Proceedings of the London Mathematical Society 102, 2 (2011), 370–394. https://doi.org/10.1112/plms/pdq026

[9]

Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. Ph.D. Dissertation. Université Nice Sophia Antipolis. arXiv:1606.05916

[10]

Ulrik Buchholtz and Jonathan Weinberger. 2021. Synthetic fibered (∞, 1)-category theory. CoRR abs/2105.01724(2021). arXiv:2105.01724

[11]

Mitchell Buckley. 2014. Fibred 2-categories and bicategories. Journal of Pure and Applied Algebra 218, 6 (2014), 1034–1074. https://doi.org/10.1016/j.jpaa.2013.11.002

[12]

Thierry Coquand, Bassel Mannaa, and Fabian Ruch. 2017. Stack semantics of type theory. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 1–11. https://doi.org/10.1109/LICS.2017.8005130

[13]

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raussen. 2016. Directed Algebraic Topology and Concurrency. Springer. https://doi.org/10.1007/978-3-319-15398-8

[14]

Eric Finster and Samuel Mimram. 2017. A type-theoretical definition of weak ω-categories. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 1–12. https://doi.org/10.1109/LICS.2017.8005124

[15]

Eric Finster, David Reutter, Alex Rice, and Jamie Vicary. 2022. A Type Theory for Strictly Unital -Categories. In 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (LICS ’22). https://doi.org/10.1145/3531130.3533363

Digital Library

[16]

Marcelo Fiore and Philip Saville. 2019. A type theory for cartesian closed bicategories (Extended Abstract). In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. IEEE, 1–13. https://doi.org/10.1109/LICS.2019.8785708

[17]

Richard Garner. 2009. Two-dimensional models of type theory. Math. Struct. Comput. Sci. 19, 4 (2009), 687–736. https://doi.org/10.1017/S0960129509007646

Digital Library

[18]

John W. Gray. 1966. Fibred and Cofibred Categories. In Proceedings of the Conference on Categorical Algebra, S. Eilenberg, D. K. Harrison, S. MacLane, and H. Röhrl (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 21–83. https://doi.org/10.1007/978-3-642-99902-4_2

[19]

Claudio Hermida. 1999. Some properties of Fib as a fibred 2-category. Journal of Pure and Applied Algebra 134, 1 (1999), 83–109. https://doi.org/10.1016/S0022-4049(97)00129-1

[20]

Tom Hirschowitz. 2013. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Log. Methods Comput. Sci. 9, 3 (2013). https://doi.org/10.2168/LMCS-9(3:10)2013

[21]

Martin Hofmann and Thomas Streicher. 1994. The Groupoid Model Refutes Uniqueness of Identity Proofs. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS ’94), Paris, France, July 4-7, 1994. IEEE Computer Society, 208–212. https://doi.org/10.1109/LICS.1994.316071

[22]

André Joyal and Ross Street. 1993. Pullbacks equivalent to pseudopullbacks. Cahiers de topologie et géométrie différentielle catégoriques 34, 2 (1993), 153–156. http://eudml.org/doc/91518

[23]

Krzysztof Kapulkin and Peter LeFanu Lumsdaine. 2021. The simplicial model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society 23, 6 (2021), 2071–2126. https://doi.org/10.4171/jems/1050

[24]

Daniel R. Licata. 2011. Dependently Typed Programming with Domain-Specific Logics. Ph.D. Dissertation. USA. Advisor(s) Harper, Robert. https://doi.org/10.5555/2338432 AAI3476124.

Digital Library

[25]

Daniel R. Licata and Robert Harper. 2011. 2-Dimensional Directed Type Theory. In Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011(Electronic Notes in Theoretical Computer Science, Vol. 276), Michael W. Mislove and Joël Ouaknine (Eds.). Elsevier, 263–289. https://doi.org/10.1016/j.entcs.2011.09.026

Digital Library

[26]

Daniel R. Licata and Robert Harper. 2012. Canonicity for 2-dimensional type theory. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, John Field and Michael Hicks (Eds.). ACM, 337–348. https://doi.org/10.1145/2103656.2103697

Digital Library

[27]

Fosco Loregian and Emily Riehl. 2020. Categorical notions of fibration. Expositiones Mathematicae 38, 4 (2020), 496–514. https://doi.org/10.1016/j.exmath.2019.02.004

[28]

Peter LeFanu Lumsdaine. 2010. Weak omega-categories from intensional type theory. Log. Methods Comput. Sci. 6, 3 (2010). https://doi.org/10.2168/LMCS-6(3:24)2010

[29]

Paige Randall North. 2019. Towards a Directed Homotopy Type Theory. In Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2019, London, UK, June 4-7, 2019(Electronic Notes in Theoretical Computer Science, Vol. 347), Barbara König (Ed.). Elsevier, 223–239. https://doi.org/10.1016/j.entcs.2019.09.012

Digital Library

[30]

Andreas Nuyts. 2015. Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance. Master’s thesis. KU Leuven. https://anuyts.github.io/files/mathesis.pdf

[31]

David Reutter and Jamie Vicary. 2019. High-level methods for homotopy construction in associative n-categories. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. IEEE, 1–13. https://doi.org/10.1109/LICS.2019.8785895

[32]

Emily Riehl and Michael Shulman. 2017. A type theory for synthetic ∞-categories. Higher Structures 1, 1 (May 2017), 147–224. https://journals.mq.edu.au/index.php/higher_structures/article/view/36

[33]

Robert A. G. Seely. 1987. Modelling Computations: A 2-Categorical Framework. In Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Ithaca, New York, USA, June 22-25, 1987. IEEE Computer Society, 65–71.

[34]

Michael Shulman. 2010. Functorially Dependent Types. https://ncatlab.org/michaelshulman/show/functorially+dependent+types

[35]

Michael Shulman. 2011. Internal Logic of a 2-Category. https://ncatlab.org/michaelshulman/show/internal+logic+of+a+2-category

[36]

Michael Shulman. 2012. 2-Categorical Logic. https://ncatlab.org/michaelshulman/show/2-categorical+logic

[37]

Michael Shulman. 2019. Fibrational Slice. https://ncatlab.org/michaelshulman/show/fibrational+slice

[38]

Ross Street. 1980. Fibrations in bicategories. Cahiers de topologie et géométrie différentielle catégoriques 21, 2 (1980), 111–160. http://archive.numdam.org/item/CTGDC_1980__21_2_111_0/

[39]

Ross Street. 1982. Characterization of bicategories of stacks. In Category Theory(Lecture Notes in Mathematics, Vol. 962), K.H. Kamps, D. Pumplün, and W. Tholen (Eds.). Springer. https://doi.org/10.1007/BFb0066909

[40]

Nicolas Tabareau. 2011. Aspect oriented programming: a language for 2-categories. In Proceedings of the 10th international workshop on Foundations of aspect-oriented languages, FOAL 2011, Porto de Galinhas, Brazil, March 21-25, 2011, Hridesh Rajan (Ed.). ACM, 13–17. https://doi.org/10.1145/1960510.1960514

Digital Library

[41]

The Coq Development Team. 2022. The Coq Proof Assistant. https://doi.org/10.5281/zenodo.5846982

[42]

Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, 2022. UniMath — a computer-checked library of univalent mathematics. Available at https://unimath.org. https://github.com/UniMath/UniMath

[43]

Matthew Z. Weaver and Daniel R. Licata. 2020. A Constructive Model of Directed Univalence in Bicubical Sets. In LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 915–928. https://doi.org/10.1145/3373718.3394794

Digital Library

Cited By

Ahrens BNorth Pvan der Weide N(2023)Bicategorical type theory: semantics and syntaxMathematical Structures in Computer Science10.1017/S096012952300031233:10(868-912)Online publication date: 17-Oct-2023
https://doi.org/10.1017/S0960129523000312
New MLicata D(2023)A Formal Logic for Formal Category TheoryFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_6(113-134)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30829-1_6

Recommendations

2-Dimensional Directed Type Theory

Recent work on higher-dimensional type theory has explored connections between Martin-Lof type theory, higher-dimensional category theory, and homotopy theory. These connections suggest a generalization of dependent type theory to account for ...
Canonicity for 2-dimensional type theory
POPL '12

Higher-dimensional dependent type theory enriches conventional one-dimensional dependent type theory with additional structure expressing equivalence of elements of a type. This structure may be employed in a variety of ways to capture rather coarse ...
Decidability of conversion for type theory in type theory

Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

August 2022

817 pages

ISBN:9781450393515

DOI:10.1145/3531130

Editor:
Christel Baier

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 August 2022

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Conference

LICS '22

Sponsor:

SIGLOG

LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science

August 2 - 5, 2022

Haifa, Israel

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
420
Total Downloads

Downloads (Last 12 months)202
Downloads (Last 6 weeks)67

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ahrens BNorth Pvan der Weide N(2023)Bicategorical type theory: semantics and syntaxMathematical Structures in Computer Science10.1017/S096012952300031233:10(868-912)Online publication date: 17-Oct-2023
https://doi.org/10.1017/S0960129523000312
New MLicata D(2023)A Formal Logic for Formal Category TheoryFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_6(113-134)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30829-1_6

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents