(n m : nat) : Join (Sphere n.-1) (Sphere m.-1) <~> Sphere (n + m)%nat.-1. Proof. refine (_ oE equiv_functor_join _ _). 2,3: symmetry; exact (equiv_bool_pow_sphere _). refine (equiv_bool_pow_sphere _ oE _). apply join_join_power. Defined.
Require Import Basics Types. Require Import Join.Core Join.JoinAssoc Suspension Spaces.Spheres. Require Import WildCat. Require Import Spaces.Nat.Core.