Homotopy Type Theory torsion-free halving group > history

< torsion-free abelian group