Added proof of fact that transporting along constant fibration doesn't do much.
Added recursor for Circle.
Attempt at proving equivalence between Torus and Circle x Circle.