In this article, we explore the possibilities allowed by higher inductive types. They enable a much more intuitive formalization of integers and new mind-blowing definitions of the (homotopical) ci…