HoTT and Axiom K

[Mathnerd314]

https://lirias2repo.kuleuven.be/bitstream/handle/123456789/452283/icfp14-cockxA.pdf?sequence=2

I think the issue is something like evaluation erasing a homotopy path, so maybe there is a way to add some kind of path-tracing that follows beta reduction. Or, said in a less convoluted way, a way to modify reduction so that it creates/uses homotopy paths as it proceeds.

It reminds of GHC's coercion system, https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/fc-new-tyco.pdf. Constraints in GHC have evidence, as you say. Except GHC erases everything besides dictionaries; dictionaries end up being explicit arguments. This is because e.g. equality constraints are "redundant", since there is only one type equality. There's a similar idea in Idris, the elaboration system https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf, that also ends up erasing.
But I was thinking in HoTT this isn't true, because equalities are paths rather than identities. So I was thinking, for HoTT, there may be some modification to the core term calculus that carries the paths around, similar to the coercion evidence, and applies them where relevant.