`{Funext} (X : pType) : (pBool ->** X) <~>* X. Proof. snrapply Build_pEquiv'. - refine (_ oE (issig_pmap _ _)^-1%equiv). refine (_ oE (equiv_functor_sigma_pb (equiv_bool_rec_uncurried X))^-1%equiv); cbn. make_equiv_contr_basedpaths. - reflexivity. 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.