fact: Definition ptr_loops_s2_s1 `{Univalence} : pTr 1 (loops (psphere 2)) <~>* psphere 1 := (licata_finster (psphere 1))^-1*.
imports: Basics Types WildCat Pointed Truncations.Core Truncations.Connectedness Spaces.Int Spaces.Circle Spaces.Spheres Algebra.AbGroups Homotopy.HomotopyGroup Homotopy.HSpaceS1 Homotopy.Hopf