# Homotopy Type Theory halving group > history (Rev #3)

## Definition

A halving group is an abelian group G with a function $(-)/2:G \to G$ called halving and a dependent function

$p:\prod_{g:G} g/2 + g/2 = g$

## Properties

• Just as every abelian group is a $\mathbb{Z}$-bimodule, every halving group is a $\mathbb{D}$-bimodule, where $\mathbb{D}$ are the dyadic rational numbers?.

• No halving group has characteristic $2$.