Right now I am studying how reals are done in Coq, but I remember a while back watching Bauer's lectures and hearing him state that HoTT has a different and better way of defining reals that either the Cauchy sequences or Dedekind cuts. I am not sure if the same applies to Cubical Agda, but for that reason I am asking. I know that the HoTT book has a section on this, but it is too much for me at the moment.
I'd be interested seeing code examples in Cubical Agda so I can contrast them with the Coq ones.