Common nouns as types: Higher inductive types in type-theoretical semantics
Zhaohui Luo
As pointed out by Geach and others, common nouns (CNs) are special in that they have their own criteria of identity (ICs) [3]. In type-theoretical semantics, this provides a justification for the idea of interpreting CNs as types and the ICs as equivalence relations over the types, i.e., the pairs called setoids [6]. However, there is a discrepancy here in the CNs-as-types paradigm: setoids are pairs, not types. Although in most cases ICs are ‘commonly understood’ and can hence be ignored, they cannot be so ignored in sophisticated cases where it is only adequate to interpret CNs as setoids [1,7]. Furthermore, it is known that in practice working with setoids is inconvenient and direct treatments of quotient types are called for. The recent study of Higher Inductive Types [4,5,2], as a development in the research on Homotopy Type Theory as a foundational language of mathematics, has opened up a new avenue and, in particular, it enables the study of quotient types from a fresh angle with much needed computational justification of the resulting type theory. If time permits, I’ll also discuss some related ongoing research topics, albeit only briefly.
Bibliography
- S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories. Wiley/ISTE, 2020.
- T. Coquand, S. Huber, and P. Mortberg. On higher inductive types in cubical type theory. Proceedings of the 33rd Symposium on Logic in Computer Science (LICS’18), 2018.
- P. Geach. Reference and Generality. Cornell University Press, 1962. (Third edition in 1980).
- HoTT. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013.
- P. Lumsdaine and M. Shulman. Semantics of higher inductive types. Math. Proc. Camb. Phil. Soc., 169:159–208, 2020.
- Z. Luo. Common nouns as types. In D. Bechet and A. Dikovsky, editors, Logical Aspects of Computational Linguistics (LACL’2012). LNCS 7351, pages 173–185, 2012.
- Z. Luo. Modern Type Theories: Their Development and Applications. Tsinghua University Press, 2024. (In Chinese).