Gaëtan Gilbert: Formalising real numbers in homotopy type theory. CPP 2017: 112-124