The Integers as a Higher Inductive Type