Thanks Nicolai! And yes, our β' is a different definition of the order of pi_4(S^3). In fact, the number β in the Summary file is not exactly the same number as in Guillaume's Appendix B either for various reasons. For instance, Guillaume only uses 1-HITs while we are quite liberal in using higher HITs as they are not much harder to work with in Cubical Agda than 1-HITs. Also Guillaume of course defines everything with path-induction while we use cubical primitives and the maps in appendix B are quite unnecessarily complex from a cubical point of view (for instance, the equivalence S^3 = S^1 * S^1 can be written quite directly in Cubical Agda while in Book HoTT it's a bit more involved and Guillaume uses a chain of equivalences to define it).
One could of course define the number exactly like Guillaume does and try to compute it, but I don't find that very interesting now that we have a much simpler definition which is fast to compute. However, we have come up with various other interesting numbers that we can't get Cubical Agda to compute, so there's definitely room to make cubical evaluation faster. Surprisingly enough though, one doesn't need to do this in order to get Cubical Agda to compute the order of pi_4(S^3) :-)
--