proposition: Lemma loops_psigma_commute (A : pType) (P : pFam A) : loops (psigma P) <~>* psigma (loopsD P).
proof: Proof. snrapply Build_pEquiv'. 1: exact (equiv_path_sigma _ _ _)^-1%equiv. reflexivity. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core