Formalising Real Numbers in Homotopy Type Theory