The HoTT Game

This seems all well thought-out and the drawings are very well-made. However, descriptions like "We make a path p : true ≡ false from the assumed path (homotopy) h : Refl ≡ loop by constructing a non-trivial Bool-bundle over the circle, hence obtaining a map ( Refl ≡ loop ) → ⊥." are largely incomprehensible for people without an undergraduate in mathematics.

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.

It is and is not really relevant for non-mathematicians. If there is finally an digitization of the system then I suspect programmers will find it useful, but until then, it is useful for exploring mathematics separate from set theory. E.g. instead of picking one or the other for a set theory axiom, choose neither.

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.