`{Funext} n X : IsTrunc n.+2 X <~> forall (x : X), IsTrunc n.+1 (loops [X, x]). Proof. srapply equiv_iff_hprop. intro tr_loops. apply istrunc_S; intros x y. apply istrunc_S; intros p. destruct p. nrapply tr_loops. 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.