proposition: Theorem pi1_torus `{Univalence} : GroupIsomorphism (Pi 1 T) (grp_prod abgroup_Z abgroup_Z).
proof: Proof. etransitivity. 1: exact (emap (Pi 1) pequiv_torus_prod_circles). etransitivity. 1: apply grp_iso_pi_prod. apply grp_iso_prod. 1,2: apply pi1_circle. 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