  In this paper, we study finitary 1-truncated higher inductive types (HITs) in
homotopy type theory. We start by showing that all these types can be
constructed from the groupoid quotient. We define an internal notion of
signatures for HITs, and for each signature, we construct a bicategory of
algebras in 1-types and in groupoids. We continue by proving initial algebra
semantics for our signatures. After that, we show that the groupoid quotient
induces a biadjunction between the bicategories of algebras in 1-types and in
groupoids. Then we construct a biinitial object in the bicategory of algebras
in groupoids, which gives the desired algebra. From all this, we conclude that
all finitary 1-truncated HITs can be constructed from the groupoid quotient.
  We present several examples of HITs which are definable using our notion of
signature. In particular, we show that each signature gives rise to a HIT
corresponding to the freely generated algebraic structure over it. We also
start the development of universal algebra in 1-types. We show that the
bicategory of algebras has PIE limits, i.e. products, inserters and equifiers,
and we prove a version of the first isomorphism theorem for 1-types. Finally,
we give an alternative characterization of the foundamental groups of some
HITs, exploiting our construction of HITs via the groupoid quotient. All the
results are formalized over the UniMath library of univalent mathematics in
Coq.

Logic in Computer Science