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.
HoTT is certainly esoteric and impenetrable for outsiders. It could even be a bunch of gibberish technobabble and we couldn't tell the difference because there's no effort to reach outside their target group and that's quite small. People seem to praise it so perhaps some day I will be able to enjoy it as well.
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.
I wonder if services like gitpod/github codespaces/repl.it would be a good solution for allowing people to use an agda environment without installing it.
I don't know what proof is used here, but the standard proof uses univalence to upgrade the equivalence (_ + 1): Z -> Z to a path Z = Z. Then we use induction for S^1 to define the map S^1 -> U that takes the base point to Z and the loop to the path Z = Z.
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.
Lean 3 introduced singleton-elimination which is inconsistent with HoTT. There's a project [0] that uses an attribute to restrict uses of that rule, but it isn't really ergonomic to use.
Readit News
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.
[0] https://github.com/gebner/hott3
Dead Comment