The combination "try to understand the math concepts that are not explained", "deal with a programming language and syntax I've never seen before" and "deal with emacs" quickly extinguished any interest I had as a mere physicist.
That being said, I think the core issue is that I'm not in the target audience. At the same time, it's being posted in a more general forum, and I think it's important for others to know that thye shouldn't feel too frustrated when they can't figure out the goal (let alone the solution) to the exercises.
Probably applicable to finding complexity proofs as well, and optimization.
I reached, some time ago, the conclusion that you could compare programs for equality and determine if they are equal. This traversal of the graph/type theory representation of the program can be NP hard, but it may also not be, and could save lots of time in fields like automatic differentiation by pruning possible solutions that don't need to be evaluated.
To some surprise I'd found other people mentioning this as well.
My not being versed in emacs poses a little bit of an obstacle when I attempt to use it though.
Having the fundamental groupoid of the circle be the integers requires the universe to be a 1-type or higher. There are some type theories that have that without full univalence (e.g. this [0]), but it'll definitely have a HoTT flavor with non-identity paths.
[0] Two-dimensional models of type theory: https://arxiv.org/abs/0808.2122
But, I suspect the idea involves like, using the idea of equivalences from the type theory as being the paths, and such.
