The HoTT Game

The HoTT Game(homotopytypetheory.org)

96 points by VitalyAnkh 4 years ago | 12 comments

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.

epilys 4 years ago | |

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.

R0b0t1 4 years ago | | |

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.

maxbendick 4 years ago |

Category theory, type theory, and HoTT are all a joy! Worth checking out, especially if you didn't enjoy math in school.

orangea 4 years ago |

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.

ghuntley 4 years ago | |

Howdy, Geoff from Gitpod here. Yes, I just created this for the Agda community. Enjoy <3 https://github.com/gitpod-io/template-agda

drdeca 4 years ago | |

there is one on agdapad at https://agdapad.quasicoherent.io/ (linked in the comments on the linked page)

My not being versed in emacs poses a little bit of an obstacle when I attempt to use it though.

orangea 4 years ago |

Does the "fundamental group of the circle" part use anything specifically from homotopy type theory as opposed to any other type theory?

scapp 4 years ago | |

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.

[0] Two-dimensional models of type theory: https://arxiv.org/abs/0808.2122

drdeca 4 years ago | |

I suspect the answer is yes, because it seems particularly well suited for that, but I haven't really gotten far enough into it to say for sure.

But, I suspect the idea involves like, using the idea of equivalences from the type theory as being the paths, and such.

dqpb 4 years ago |

Wonder why they didn’t do it in Lean?

scapp 4 years ago | |

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.

[0] https://github.com/gebner/hott3