I'm afraid homotopy type theory has zero relevance towards anything related to applied programming at this stage, especially if you are not already an academic

I'm afraid homotopy type theory has zero relevance towards anything related to applied programming at this stage, especially if you are not already an academic doing PHD-level research. if you want to learn some functional programming along with abstractions actually used in FP programming, that is one thing, but that is not homotopy type theory, which is squarely in the domain of purely abstract mathematics which would be interesting from a pure mathematics perspective, not a programming perspective. The paper does appear to include some proof that utilize Coq, but unless you're interested in software that checks the validity of mathematical proofs, that is not going to help you get a more interesting programming job.