{A} : pFam A -> pFam (loops A) := fun Pp => Build_pFam (fun q : loops A => transport Pp q (dpoint Pp) = (dpoint Pp)) 1. Global Instance istrunc_pfam_loopsD {n} {A} (P : pFam A) {H :IsTrunc_pFam n.+1 P} : IsTrunc_pFam n ( P). Proof. intros a. pose (H (point A)). exact _. 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.