It really is remarkable. I think the most remarkable fact about it is that the intensional identity type was invented by Martin Lof in the 70s, the groupoid model was discovered in the 90s and then finally in the late 2000s various people made the connection that Martin Lof's original system from the 70s was in a sense already a type theory for abstract homotopy theory. This led to an explosion of new ideas in type theory (univalence, higher inductive types, modalities) that took a somewhat obscure field of math/cs to the thriving research community it is today.
I’ll admit to coming late to the party (when a friend introduced me in 2013), but what’s amazing to me is when you take the step of encoding your cellular structures as adjacency matrices.
You can visually see structures of your theory (eg, facts about groups) in the patterns of terms in the matrix.
Eg, diagramming a cyclic group ends up with a banding pattern in the portion of your matrix denoting equivalent pairs under the operation… which shows that in some sense, the level maps of + on Zn x Zn form a twisted torus. (Which makes sense in hindsight, as you have the product of two loops with the level maps wrapping around non-trivially.)
That you get ideas such as that by chasing through a purely abstract definition (groups -> diagrams) is wild to me.
Edit:
I actually built a simple case (Z4) in Minecraft — just because I found it surprising.
