From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import Join.Core Join.JoinAssoc Suspension Spaces.Spheres.
From HoTT.WildCat Require Import Core Universe Equiv.
Require Import Spaces.Nat.Core.

(** * [Join Bool A] is equivalent to [Susp A]

  We give a direct proof of this fact. It is also possible to give a proof using [opyon_equiv_0gpd]; see PR#1769. *)

Definition join_to_susp (A : Type) : Join Bool A -> Susp A.
A: Type
Join Bool A -> Susp A
Proof.
A: Type
Join Bool A -> Susp A
  srapply Join_rec.
A: Type
Bool -> Susp A
A: Type
A -> Susp A
A: Type
forall (a : Bool) (b : A), ?P_A a = ?P_B b
  -
A: Type
Bool -> Susp A exact (fun b => if b then North else South).
  -
A: Type
A -> Susp A exact (fun a => South).
  -
A: Type
forall (a : Bool) (b : A),
(fun b0 : Bool => if b0 then North else South) a = (fun _ : A => South) b intros [|] a.
A: Type
a: A
North = South
A: Type
a: A
South = South
    +
A: Type
a: A
North = South exact (merid a).
    +
A: Type
a: A
South = South reflexivity.
Defined.

Definition susp_to_join (A : Type) : Susp A -> Join Bool A.
A: Type
Susp A -> Join Bool A
Proof.
A: Type
Susp A -> Join Bool A
  srapply (Susp_rec (joinl true) (joinl false)).
A: Type
A -> joinl true = joinl false
  exact (zigzag true false).
Defined.

Instance isequiv_join_to_susp (A : Type) : IsEquiv (join_to_susp A).
A: Type
IsEquiv (join_to_susp A)
Proof.
A: Type
IsEquiv (join_to_susp A)
  snapply (isequiv_adjointify _ (susp_to_join A)).
A: Type
join_to_susp A o susp_to_join A == idmap
A: Type
susp_to_join A o join_to_susp A == idmap
  -
A: Type
join_to_susp A o susp_to_join A == idmap snapply Susp_ind.
A: Type
(fun y : Susp A => (join_to_susp A o susp_to_join A) y = idmap y) North
A: Type
(fun y : Susp A => (join_to_susp A o susp_to_join A) y = idmap y) South
A: Type
forall x : A,
transport (fun y : Susp A => (join_to_susp A o susp_to_join A) y = idmap y)
  (merid x) ?H_N =
?H_S
    1,2: reflexivity.
A: Type
forall x : A,
transport (fun y : Susp A => (join_to_susp A o susp_to_join A) y = idmap y)
  (merid x) 1 =
1
    intros a; cbn beta.
A: Type
a: A
transport (fun y : Susp A => join_to_susp A (susp_to_join A y) = y) 
  (merid a) 1 =
1
    transport_paths FFlr.
A: Type
a: A
ap (join_to_susp A) (ap (susp_to_join A) (merid a)) @ 1 = 1 @ merid a
    apply equiv_p1_1q.
A: Type
a: A
ap (join_to_susp A) (ap (susp_to_join A) (merid a)) = merid a
    lhs napply (ap _ _); [napply Susp_rec_beta_merid | ].
A: Type
a: A
ap (join_to_susp A) (zigzag true false a) = merid a
    lhs napply (Join_rec_beta_zigzag _ _ _ true false a).
A: Type
a: A
merid a @ 1^ = merid a
    apply concat_p1.
  -
A: Type
susp_to_join A o join_to_susp A == idmap srapply (Join_ind_FFlr (join_to_susp A)); cbn beta.
A: Type
forall a : Bool, susp_to_join A (join_to_susp A (joinl a)) = joinl a
A: Type
forall b : A, susp_to_join A (join_to_susp A (joinr b)) = joinr b
A: Type
forall (a : Bool) (b : A),
ap (susp_to_join A) (ap (join_to_susp A) (jglue a b)) @ ?Goal0 b =
?Goal a @ jglue a b
    1: intros [|]; reflexivity.
A: Type
forall b : A, susp_to_join A (join_to_susp A (joinr b)) = joinr b
A: Type
forall (a : Bool) (b : A),
ap (susp_to_join A) (ap (join_to_susp A) (jglue a b)) @ ?Goal b =
(fun a0 : Bool =>
 if a0 as b0 return (susp_to_join A (join_to_susp A (joinl b0)) = joinl b0)
 then 1
 else 1) a @
jglue a b
    1: intros a; apply jglue.
A: Type
forall (a : Bool) (b : A),
ap (susp_to_join A) (ap (join_to_susp A) (jglue a b)) @
(fun a0 : A => jglue false a0) b =
(fun a0 : Bool =>
 if a0 as b0 return (susp_to_join A (join_to_susp A (joinl b0)) = joinl b0)
 then 1
 else 1) a @
jglue a b
    intros b a; cbn beta.
A: Type
b: Bool
a: A
ap (susp_to_join A) (ap (join_to_susp A) (jglue b a)) @ jglue false a =
(if b as b0 return (susp_to_join A (join_to_susp A (joinl b0)) = joinl b0)
 then 1
 else 1) @
jglue b a
    lhs nrefine (ap _ _ @@ 1).
A: Type
b: Bool
a: A
ap (join_to_susp A) (jglue b a) = ?Goal
A: Type
b: Bool
a: A
ap (susp_to_join A) ?Goal @ jglue false a =
(if b as b0 return (susp_to_join A (join_to_susp A (joinl b0)) = joinl b0)
 then 1
 else 1) @
jglue b a
    1: napply Join_rec_beta_jglue.
A: Type
b: Bool
a: A
ap (susp_to_join A)
  ((if b as b0 return (A -> (if b0 then North else South) = South)
    then fun a0 : A => merid a0
    else fun _ : A => 1) a) @
jglue false a =
(if b as b0 return (susp_to_join A (join_to_susp A (joinl b0)) = joinl b0)
 then 1
 else 1) @
jglue b a
    destruct b.
A: Type
a: A
ap (susp_to_join A) (merid a) @ jglue false a = 1 @ jglue true a
A: Type
a: A
ap (susp_to_join A) 1 @ jglue false a = 1 @ jglue false a
    +
A: Type
a: A
ap (susp_to_join A) (merid a) @ jglue false a = 1 @ jglue true a rhs napply concat_1p.
A: Type
a: A
ap (susp_to_join A) (merid a) @ jglue false a = jglue true a
      lhs nrefine (_ @@ 1); [napply Susp_rec_beta_merid | ].
A: Type
a: A
zigzag true false a @ jglue false a = jglue true a
      apply concat_pV_p.
    +
A: Type
a: A
ap (susp_to_join A) 1 @ jglue false a = 1 @ jglue false a reflexivity.
Defined.

Definition equiv_join_susp (A : Type) : Join Bool A <~> Susp A
  := Build_Equiv _ _ (join_to_susp A) _.

(** It follows that the join powers of [Bool] are spheres.  These are sometimes a convenient alternative to working with spheres, so we give them a name. *)
Definition bool_pow (n : nat) := join_power Bool n.

Definition equiv_bool_pow_sphere (n : nat): bool_pow n <~> Sphere (n.-1).
n: nat
bool_pow n <~> Sphere n.-1
Proof.
n: nat
bool_pow n <~> Sphere n.-1
  induction n as [|n IHn].
bool_pow 0 <~> Sphere 0%nat.-1
n: nat
IHn: bool_pow n <~> Sphere n.-1
bool_pow n.+1 <~> Sphere n.+1%nat.-1
  -
bool_pow 0 <~> Sphere 0%nat.-1 reflexivity.
  -
n: nat
IHn: bool_pow n <~> Sphere n.-1
bool_pow n.+1 <~> Sphere n.+1%nat.-1 simpl.
n: nat
IHn: bool_pow n <~> Sphere n.-1
Join Bool (bool_pow n) <~> Sphere (trunc_index_inc (-2) n).+2  refine (_ oE equiv_join_susp _).
n: nat
IHn: bool_pow n <~> Sphere n.-1
Susp (bool_pow n) <~> Sphere (trunc_index_inc (-2) n).+2
    exact (emap Susp IHn).
Defined.

(** It follows that joins of spheres are spheres, starting in dimension -1. *)
Definition equiv_join_sphere (n m : nat)
  : Join (Sphere n.-1) (Sphere m.-1) <~> Sphere (n + m)%nat.-1.
n, m: nat
Join (Sphere n.-1) (Sphere m.-1) <~> Sphere (n + m)%nat.-1
Proof.
n, m: nat
Join (Sphere n.-1) (Sphere m.-1) <~> Sphere (n + m)%nat.-1
  refine (_ oE equiv_functor_join _ _).
n, m: nat
Join ?Goal0 ?Goal1 <~> Sphere (n + m)%nat.-1
n, m: nat
Sphere n.-1 <~> ?Goal0
n, m: nat
Sphere m.-1 <~> ?Goal1
  2,3: symmetry; exact (equiv_bool_pow_sphere _).
n, m: nat
Join (bool_pow n) (bool_pow m) <~> Sphere (n + m)%nat.-1
  refine (equiv_bool_pow_sphere _ oE _).
n, m: nat
Join (bool_pow n) (bool_pow m) <~> bool_pow (n + m)
  apply join_join_power.
Defined.