Cubical type theory, or any constructive interpretation of HoTT implies the computability of various aspects of algebraic topology. That means, you can encode concepts of homotopy theory into $\lambda$-terms, and use computers to do what only mathematicians could do before. In particular, it shows lots of boolean values, natural numbers, integers or functions of numbers you may find in homotopy theory textbooks/papers can be computed by certain Turing machines.
Brunerie number is an example, as is already mentioned. One should notice that, it is a special case of Whitehead product, which is an operation defined on homotopy groups for any types, and the so-called Brunerie number is all about using a natural number (instead of abstract terms) to encode the Whitehead product $[\iota,\iota]$ of 2-sphere's identity element with itself. People talk about the number more often because it is the one related to $\pi_4(S^3)$. Every Whitehead product could be computed in this way if you are able to make such an encoding. So it satisfies the criterion of @Maximilian Doré, I suppose:)
Unfortunately, it only guarantees the existence of algorithms for homotopy-theoretic computation, or one would say it provides a universal algorithm through normalization. Whatever, up to now it is far from being efficient enough to be run on an existing computer... But I have confidence that someone will find the way out eventually.
The point is, general results about computability are very rare in homotopy theory before constructive HoTT is invented. I only heard about one general theory, the spaces with effective homology, and based on that people built the Kenzo program. It can be used to compute Eilenberg-Moore spectral sequences, the homology of loop spaces and homotopy groups of spheres. Impressive, indeed, but not all-around. I'm not sure if it can compute the Whitehead product. Kenzo can run on your laptop. However, things like cubical type theory could recover all these achievements and much more, at least in theory.