Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just generalized algebraic data types and [non-truncated quotients](https://github.com/agda/cubical/blob/5c22f5dcaaddaeb7f07dfa46ece5fe486947df44/Cubical/HITs/TypeQuotients/Base.agda)?