Fundamental Group of S¹
================

Prerequisites :
- circle 
- loop space
- have useless maps pi(S¹) → ℤ and ℤ → pi(S¹)




- we make helix from ℤ ≡ ℤ

- 

Motivating Steps :
0. After sufficient pondering, you guess that
   loops are determined by how many times they go around
1. Count number of times loops go around using ℤ
   by setting the single loop to +1.
2. You can make a comparison maps between loop space and ℤ
   but can't yet show an equivalence
3. You realize you need to use the definition of S¹,
   so you go from `base ≡ base ≃ Z` to  `base ≡ x ≃ Bundle x`.
   i.e. You try to make the equivalence _over_ S¹


Random thought : 
to prove `a = b`, we realise that `a = f(x0)` 
and `b = g(x0)` for `x0 : X`,
and instead show `(x : X) → f x = g x`.
This turns out to be easier since we now get 
access to the recursor of `X`.