Homotopy Type Theory Z-algebra > history

< nonassociative ring