TY - RPRT TI - The Cayley-Dickson Construction in Homotopy Type Theory AU - Ulrik Buchholtz AU - Egbert Rijke PY - 2016 UR - https://arxiv.org/abs/1610.01134 ID - 1610.01134 ER -