The core sentence of the post comes a bit later, just above the "Conclusion" section header: "This type theory is used in proof assistants such as Coq and Agda;

The core sentence of the post comes a bit later, just above the "Conclusion" section header: "This type theory is used in proof assistants such as Coq and Agda; eventually, this expressive logic + dependent types will be utilized in many programming languages." Note the "is used" part, which is in the present tense. My understanding is that nothing new was constructed here. Maybe the well-known theory of dependent types has been reconstructed in a new way based on categories; this may be exciting to fans of category theory, but I don't see how it advances programming languages in any way. The actual paper isn't any more helpful either: It name-drops JavaScript in the introduction and at the very end, but doesn't really do anything with it, it certainly doesn't show any kind of model of a type system for even a trivial JavaScript subset.