proposition: Theorem pi1_circle : Pi 1 [Circle, base] ≅ abgroup_Z.
proof: Proof. symmetry. srapply Build_GroupIsomorphism'. { equiv_via (base = base). 2: exact (equiv_tr 0 (loops [Circle, base])). symmetry. exact equiv_loopCircle_int. } intros a b. cbn; apply ap. apply loopexp_add. Defined.
imports: Basics Types WildCat Pointed Truncations.Core Truncations.Connectedness Spaces.Int Spaces.Circle Spaces.Spheres Algebra.AbGroups Homotopy.HomotopyGroup Homotopy.HSpaceS1 Homotopy.Hopf