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.
Require Import Pointed.Core Pointed.pEquiv Pointed.pSusp.

Local Open Scope pointed_scope.

(** * [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 =>
 match
   a0 as b0 return susp_to_join A (join_to_susp A (joinl b0)) = joinl b0
 with
 | true => 1
 | false => 1
 end) 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 =>
 match
   a0 as b0 return susp_to_join A (join_to_susp A (joinl b0)) = joinl b0
 with
 | true => 1
 | false => 1
 end) 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 =
match
  b as b0 return susp_to_join A (join_to_susp A (joinl b0)) = joinl b0
with
| true => 1
| false => 1
end @ 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 =
match
  b as b0 return susp_to_join A (join_to_susp A (joinl b0)) = joinl b0
with
| true => 1
| false => 1
end @ jglue b a
    1: napply Join_rec_beta_jglue.
A: Type
b: Bool
a: A
ap (susp_to_join A)
  (match b as b0 return A -> (if b0 then North else South) = South with
   | true => fun a0 : A => merid a0
   | false => fun _ : A => 1
   end a) @
jglue false a =
match
  b as b0 return susp_to_join A (join_to_susp A (joinl b0)) = joinl b0
with
| true => 1
| false => 1
end @ 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.

(** A pointed version of [equiv_join_sphere], starting in dimension 0. *)
Definition pequiv_pjoin_sphere (n m : nat)
  : pjoin (psphere n) (Sphere m) <~>* psphere (n + m.+1)%nat
  := Build_pEquiv' (equiv_join_sphere n.+1 m.+1) 1.

(** The suspension of a join is the join with one factor suspended. *)
Definition equiv_susp_join (A B : Type)
  : Susp (Join A B) <~> Join (Susp A) B
  := equiv_functor_join (equiv_join_susp A) equiv_idmap
       oE join_assoc Bool A B
       oE (equiv_join_susp (Join A B))^-1%equiv.

Definition pequiv_psusp_join (A B : Type)
  : psusp (Join A B) <~>* pjoin (psusp A) B
  := Build_pEquiv' (equiv_susp_join A B) 1.

(** * Diamonds in the self-join of a suspension *)

(** This is used in CayleyDickson.v. *)
Definition diamond_susp {A : Type} (t : Susp A)
  : diamond South t North t.
A: Type
t: Susp A
diamond South t North t
Proof.
A: Type
t: Susp A
diamond South t North t
  revert t; snapply Susp_ind; cbn beta.
A: Type
diamond South North North North
A: Type
diamond South South North South
A: Type
forall x : A,
transport (fun y : Susp A => diamond South y North y) (merid x) ?Goal =
?Goal0
  -
A: Type
diamond South North North North exact (diamond_v South North 1).
  -
A: Type
diamond South South North South exact (diamond_h North South 1).
  -
A: Type
forall x : A,
transport (fun y : Susp A => diamond South y North y) 
  (merid x) (diamond_v South North 1) =
diamond_h North South 1 intro a.
A: Type
a: A
transport (fun y : Susp A => diamond South y North y) 
  (merid a) (diamond_v South North 1) =
diamond_h North South 1
    apply diamond_twist.
Defined.