(A : Type) : Join Bool A -> Susp A. Proof. srapply Join_rec. - exact (fun b => if b then North else South). - exact (fun a => South). - intros [|] a. + exact (merid a). + reflexivity. Defined.
Require Import Basics Types. Require Import Join.Core Join.JoinAssoc Suspension Spaces.Spheres. Require Import WildCat. Require Import Spaces.Nat.Core.