proposition: Theorem loops_torus `{Univalence} : loops T <~>* Int * Int.
proof: Proof. refine (_ o*E pequiv_ptr (n:=0)). nrapply pi1_torus. Defined.
imports: Basics Types Pointed WildCat Modalities.ReflectiveSubuniverse Truncations.Core Algebra.AbGroups Homotopy.HomotopyGroup Homotopy.PinSn Spaces.Int.Core Spaces.Circle Spaces.Torus.Torus Spaces.Torus.TorusEquivCircles