Out of curiosity as someone less mathematically inclined but very interested in mathematics: what do you do with the equations in books like this?
Do you look at them and already intuitively know what they mean so you don't have to dig deeper? Do you slowly go over each element individually and then grasp the whole thing afterwards? Or are you so used to them that you can read them more or less the way you read English? I really want go deeper into this stuff but when I look at these books I feel like I would need years of specialized training to understand them.
Written mathematics is quite informationally dense and, in general, reads much more slowly than typical English prose. Sometimes you do have to go over an equation symbol-by-symbol; sometimes you have to convince yourself of the truth of a sentence with no symbols at all.
Disclaimer: I am a self taught pleb, not a mathematician.
The pdf blows up my phone but the first equations look like basic calculus, and the rest seem to be in the form of logical judgments where above the horizontal line are called the premises of the rule, and the judgment below the line is called its conclusion. I've seen Godel's T (System T) used in this style, and it seems this pdf is using set theory (again, my shit phone explodes and can't load half the pages) though I would imagine these would be done in category theory these days.
To "understand" math, (scare quotes because again, I'm just a pleb), you really need to know what field, or set of axioms, or universe you're working in. The rational numbers are the easiest imho, when you get into the reals you're dealing with mathematical objects that may not even be possible to be represented as numbers (as I understand it) so if you can understand symbolic programming ala Sussman Lisp/Scheme you can understand math just you're unfamiliar with the notation, and unfamilar with whatever the rules of this particular abstraction are, that's all. By axioms I mean somebody has merely stated "I created this universe, here are the axioms that rule this abstract universe" meaning they often will not be congruent with any kind of other fields/axioms, in my experience as a plebmatician.
If you want to understand there's a guy from here who wrote a book https://pimbook.org/ and to get into Per Martin-Löf you'll probably need some logic courses, professor Robert Harper or Frank Pfenning both have 'intuitionistic' constructivist math resources you can read/learn from if you google.
I had exactly the same question. Until just last year. (I’m 39.)
We’re all different, especially in how we process abstract concepts. I process them quite visually. Among my friends it seems there is some correlation between having a maths degree and thinking directly in the math symbols.
What I have tried to do is just to power through. Scanning and jumping over the paper I try to construct a mental model that the equation is a blueprint for. This is this. This is that. There’s a relation here. What is it. Ah yes it’s just that here. And that is then ... yes.
Usually when i get the equation it’s much simpler than I assume at first. It’s just the ideas in a couple of paragraphs put together in an unambiguous way.
So I just kind of power through! And it can and does take some time! But once through it tends to stick. it’s quite cool.
Here’s more: https://github.com/michaelt/martin-lof
Here’s another one - this one is wonderful: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Bo...
As far as I understand the theory, then dependently typed languages such as Idris have their roots in his work on intuitionistic type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory
Intuitionism in math is beautiful imo: https://en.wikipedia.org/wiki/Intuitionism