The HoTT Game
homotopytypetheory.org
The HoTT Game
1–10 of 14 posts
Re: The HoTT Game
#2Wonder why they didn’t do it in Lean?
Re: The HoTT Game
#3Category theory, type theory, and HoTT are all a joy! Worth checking out, especially if you didn't enjoy math in school.
Re: The HoTT Game
#4Wonder why they didn’t do it in Lean?
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.
Re: The HoTT Game
#5I appreciate that mathematicians are still finding havens of abstraction to retreat to in the midst of a deranged and chaotic political climate.
Re: The HoTT Game
#6Does the "fundamental group of the circle" part use anything specifically from homotopy type theory as opposed to any other type theory?
Re: The HoTT Game
#7I 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.
Re: The HoTT Game
#8I 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.
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.
Re: The HoTT Game
#9Does the "fundamental group of the circle" part use anything specifically from homotopy type theory as opposed to any other type theory?
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.
Re: The HoTT Game
#10Does the "fundamental group of the circle" part use anything specifically from homotopy type theory as opposed to any other type theory?
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