Homotopy Type Theory domain (ring theory) > history

< integral domain