# Is it fair to say that Martin Löf Type Theory is doing the same for maths as what type theory did for programming languages?

Let me clarify what I mean.

I am currently writing a dissertation on ML/Homotopy type theory as someone who is more of a theoretical computer scientist than an Algebraist. My dissertation is focused on talking about foundations of HoTT in mostly computer scientific terminology (trying to avoid Cat theory as much as possible) and looking at canonicity/computability of it (the main result highlighted in the dissertation is canonicity of 2DTT).

When talking to my dad who is a programmer about it, I was trying to find ways to convey to him what HoTT is and why is it useful. What I discovered recently is that it helps to draw parallels between programming languages and mathematical foundations. Set Theory is kinda like Assembly, you represent complex structures in terms of basic building blocks (binary/basic sets); a function that is intended to be applied to integers can in theory be applied to strings as they have same underlying structure and there is nothing stopping you from doing so, as a set representing a number and same set representing a string are technically the same. On the other hand MLTT is like a strictly typed language, every variable is given a type for life. In order to define a new type, you need to make the structure on that type clear (constructors) and to apply any function to an element of a type you need a function on that exact type. Polymorphism is handled through adjoint types. And what I found particularly useful in conveying what HoTT is about is pointing out that identity types are kind of like overriding equality of a type. A standard equality in strictly typed languages is pointer equality, for variables that refer to literally the same physical token. However you can override equality with a function that equates more types. And if you want the equality to function properly (so, for equal elements to always be interchangeable like univalence axiom demands) you need the equality to have computational content of coercing between the two elements, just like in HoTT.

Noticing this made me think - is there a larger philosophical way in which HoTT is doing for maths what strongly typed languages did to programming languages - allow us to work at a higher language of abstraction since a lot of "safety" concerned are handled by the language itself?

• It would be very helpful if you gave a concrete example of how HoTT achieves "allow use to work at a higher language of abstraction" and how that is helpful for mathematics. Also, how is this better than category theory. How do you think "safety" is defined for mathematics? Apr 8, 2023 at 21:50

In my mind, your proposed analogy $$(\text{set theory} \leftrightarrow \text{assembly})$$ and $$(\text{type theory} \leftrightarrow \text{higher PL})$$ is not quite suitable: I would agree that set theory likens assembly in that, simultaneously, (a) you can express everything you want, (b) you can express many things you don't want -- a primary source for (b) being the lack of typing in set theory and assembly. However, where used as a foundational system, type theory rather serves as an alternative 'assembly' which avoids (b), not something built atop of it -- like an alternative choice of Turing complete 'base' language. When you model type theory in set theory, this is like simulating one Turing complete language by another. Finally, compiling a higher language down to assembly corresponds to the (often informal) practice of building a tower of definitions on upon set theory and reasoning in terms of those, which (luckily) leads to the specifics of the underlying set-theory quickly becoming largely irrelevant to the working mathematician.