Division by Two, in Homotopy Type Theory