3 ms·
Does the "fundamental group of the circle" part use anything specifically from homotopy type theory as opposed to any other type theory?
by orangea 5y ago
Does the "fundamental group of the circle" part use anything specifically from homotopy type theory as opposed to any other type theory?
- drdeca 5y agoI 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.
- scapp 5y agoI 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 https://arxiv.org/abs/0808.2122