University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > One-Dimensional Higher Inductive Types

One-Dimensional Higher Inductive Types

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity