(n : nat): bool_pow n <~> Sphere (n.-1). Proof. induction n as [|n IHn]. - reflexivity. - simpl. refine (_ oE equiv_join_susp _). exact (emap Susp IHn). Defined.
Require Import Basics Types. Require Import Join.Core Join.JoinAssoc Suspension Spaces.Spheres. Require Import WildCat. Require Import Spaces.Nat.Core.