Higher inductive types allow the programmer to simultaneously add equalities while defining an inductive type. This way one can define quotient types in type theory, but it is also possible to give straightforward definitions of the integers, the integers modulo 2,and finite sets of elements from a certain type.

　　The idea of higher inductive types comes from the field of "homotopy type theory", that views a proof p of an equality a=b as a path from object a to object b. This immediately generalizes to the idea that a proof q of the equality of two paths p=p' is a path transformation. On the one hand this turns type theory into an adequate language to talk about homotopies (basically: continuous transformations in space). On the other hand this has applications on how we use inductive data types in programming and how we prove properties about them.

　　In this talk we will primarily focus on the programming aspects of higher inductive types and homotopy type theory. We will mainly discuss examples of higher inductive types, how to write programs on them and how to prove properties about these programs. The talk is based on joint work by Van der Weide, Basold, Geuvers (giving a general scheme for higher inductive types) and on joint work by Van der Weide, Frumin, Gondelman, Geuvers (discussing data types for finite sets and how to implement them in the Coq proof assistant).

　　This is joint work with Van der Weide, Basold, Frumin, Gondelman.