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