Niels van der Weide, Radboud University
1-Truncated Higher Inductive Types
Higher inductive types (HITs) generalize inductive types by allowing constructors for (possibly higher) equalities in addition to point constructors. The resulting type comes together with introduction, elimination, and computation rules, which express that the type is freely generated by the given constructors. With HITs, one can define types representing topological spaces, such as the circle and the torus, but also examples from algebra, such as the integers and the free monoidal groupoid.
In homotopy type theory, types represent spaces and equality represents paths between two points. As such, equality is proof relevant, so types, including higher inductive types, have the structure of a higher groupoid. In this talk we restrict ourselves to a simpler class of types, namely the types whose equality type is described by a 1-groupoid. Such types are called 1-truncated.
In this talk, we study 1-truncated higher inductive types more closely. Our main goal is to define a signature of such HITs and show that they exist under mild conditions. We start by defining a type signatures within type theory and we define what algebras for these signatures are. In addition, we construct the initial algebra using the groupoid quotient and from that we conclude that HITs for these signatures exist. We finish by proving some results of universal algebra for the signatures we study.
This is joint work with Niccolò Veltri.