Natural Numbers in Homotopy Type Theory