Homotopy Type Theory discrete cancellation Z-algebra > history

< integral Z-algebra