`{Funext} (n : nat) (X : pType) : (psphere n ->** X) <~>* iterated_loops n X. Proof. induction n as [|n IHn]; simpl. - exact (pmap_from_bool X o*E pequiv_pequiv_precompose pequiv_S0_Bool^-1* ). - refine (emap loops IHn o*E _). refine (_ o*E loop_susp_adjoint (psphere n) _). symmetry; apply equiv_loops_ppforall. Defined.
Require Import Basics Types. Require Import WildCat.Equiv. Require Import NullHomotopy. Require Import Homotopy.Suspension. Require Import Pointed. Require Import Truncations. Require Import Spaces.Circle Spaces.TwoSphere.