Semantics of Higher Inductive Types