grouplike A3-space > history in Homotopy Type Theory