[First time posting here.. please correct me kindly if I have not followed any explicit or implicit rules. And please excuse my question if it’s vague.]
It’s exciting to see that HoTT can prove concrete homotopical results, like . It seems that to go further into other subfields, we need modality and cohesion in the theory to “buff up” the local structures – be it topological, smooth, or super-smooth..
However, I had a hard time tapping into modality and cohesion. First of, I’ve tried to understand what a cohesive topos means. As a first example of a cohesive topos, I’ve read through geometry+of+physics+–+smooth+sets and found it exciting. However, it remains unclear how to build up a theory with local model “X” from scratch by myself.
To do that, I planned to read Shulman’s proof on Brouwer’s fixed point.. hoping to understand the process by looking at a classical theorem in topology. But it is unfortunately too advanced for me, I’m not even sure where to start asking if there’s someone to help. Not being too familiar with type theory, I reckon there must be something missing.
What would you suggest if I want to quickly tap into these kind of modalic math, understand at least the proof for Brouwer fixed point, and hopefully be able to understand Schreiber’s foundation of geometry and physics?
4th year math PhD student. I’m not afraid of reading formal papers.. as long as it’s as much self-sufficient as possible. In fact, I find there’s “too much” motivation out there.. I hope to get serious, and even start to think/research in this language. Put in another way using an analogy in the world of programming: I regard Def/Thm/Proof as the source code of a program, and a regular math paper as the literate code or the manual/documentation of the source code. Sometimes it’s nice to have docs to read.. but sometimes you’d rather dive into the source code to see what it is. My mood is at the latter stage.
I’m willing to provide more details if it’d be helpful. Thank you very much!
]]>