proposition: Lemma pequiv_loops_punit : loops pUnit <~>* pUnit.
proof: Proof. snrapply Build_pEquiv'. { srapply (equiv_adjointify (fun _ => tt) (fun _ => idpath)). 1: by intros []. rapply path_contr. } reflexivity. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core