Impredicative Encodings of (Higher) Inductive Types