One-Dimensional Higher Inductive Types

Add to your list(s) Download to your calendar using vCal

• Peter Dybjer, Chalmers University of Technology
• Friday 20 January 2017, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Dominic Mulligan.

Higher inductive types are a key feature of Homotopy Type Theory. Higher inductive types generalise ordinary inductive types, by not only having constructors for elements (points), but also constructors for equalities between elements (paths), constructors for equalities between equalities, etc. In spite of their importance for the theory, the syntax and semantics of higher inductive types are not yet fully understood. To this end we look at the special case of “one-dimensional” higher inductive types (1-hits), that is, higher inductive types with only point and path constructors. A general form for an introduction rule for a 1-hit is proposed, as well as an inversion principle for deriving the elimination and equality rules from the introduction rules. We also show that the setoid model supports this schema. Finally, we outline the extension of this schema to 2-hits and their interpretation as groupoids.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.