1-Truncated Higher Inductive Types
Radboud University
Abstract: 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.