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

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.