Speaker
Zhaohui Luo
Royal Holloway, University of London
Talks at this conference:
Tuesday, 14:40, J330 
Common nouns as types: Higher inductive types in typetheoretical semantics 
As pointed out by Geach and others, common nouns (CNs) are special in that they have their own criteria of identity (ICs) [3]. In typetheoretical 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 CNsastypes 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
