The Langlands program is not similar to homotopy type theory. It is 'unifying' only in the sense that it makes striking, deep, yet very concrete[0] connections

The Langlands program is not similar to homotopy type theory. It is 'unifying' only in the sense that it makes striking, deep, yet very concrete[0] connections between 2 seemingly disparate areas of math, and because of this the tools needed to make progress in it end up touching all areas of mathematics. Homotopy type theory is more for about foundations of math stuff, i.e. which axioms you use to prove things. ZFC is by far the most common system to work within, not HTT. [0] ..despite taking years of study to understand the conjectures