My perspective is that it’s a useful idea for abstraction — which combined with category theory’s ability for composition is cool beans, at least in computer science.

The square in a category diagram is a legit object — and we can have type theories with the same features.

That’s useful for computational equivalence (eg, spec matches implementation) and path bundling to prevent case explosion.

About what you’d expect from adding homotopies to type theory.