There has been a problem on https://ncatlab.org/homotopytypetheory/show/open+problems#coquands_five_open_problems about defining a multiplication on the surreal numbers as defined in the HoTT book. For a solution, see https://arxiv.org/pdf/1812.00051.pdf.
Comments are welcome.
I can be reached at jsjean00@gmail.com.