JoinSusp.v

Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Join.Core Join.JoinAssoc Suspension Spaces.Spheres.
Require Import WildCat.
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
  intros a.A: Type
a: A
joinl true = joinl false
  exact (jglue _ a @ (jglue _ a)^).
Defined.

Global 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)
  snrapply (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 snrapply 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.A: Type
a: A
transport
  (fun y : Susp A =>
   (join_to_susp A o susp_to_join A) y = idmap y)
  (merid a) 1 = 1
    apply (transport_paths_FFlr' (f:=susp_to_join A)).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 nrapply (ap _ _); [nrapply Susp_rec_beta_merid | ].A: Type
a: A
ap (join_to_susp A) (jglue true a @ (jglue false a)^) =
merid a
    lhs nrapply (ap_pp _ _ (jglue false a)^).A: Type
a: A
ap (join_to_susp A) (jglue true a) @
ap (join_to_susp A) (jglue false a)^ = merid a
    lhs nrefine (_ @@ _).A: Type
a: A
ap (join_to_susp A) (jglue false a)^ = ?Goal0
A: Type
a: A
ap (join_to_susp A) (jglue true a) = ?Goal
A: Type
a: A
?Goal @ ?Goal0 = merid a
    1: lhs nrapply ap_V; nrapply (ap inverse).A: Type
a: A
ap (join_to_susp A) (jglue false a) = ?Goal2
A: Type
a: A
ap (join_to_susp A) (jglue true a) = ?Goal
A: Type
a: A
?Goal @ ?Goal2^ = merid a
    1,2: nrapply Join_rec_beta_jglue.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 b
  return
    (susp_to_join A (join_to_susp A (joinl b)) =
     joinl b)
 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 b
  return
    (susp_to_join A (join_to_susp A (joinl b)) =
     joinl b)
 then 1
 else 1) @ jglue b a
    1: nrapply Join_rec_beta_jglue.A: Type
b: Bool
a: A
ap (susp_to_join A)
  ((if b as b
     return
       (A -> (if b then North else South) = South)
    then fun a : A => merid a
    else fun _ : A => 1) a) @ jglue false a =
(if b as b
  return
    (susp_to_join A (join_to_susp A (joinl b)) =
     joinl b)
 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
    all: rhs nrapply concat_1p.A: Type
a: A
ap (susp_to_join A) (merid a) @ jglue false a =
jglue true a
A: Type
a: A
ap (susp_to_join A) 1 @ jglue false a = jglue false a
    +A: Type
a: A
ap (susp_to_join A) (merid a) @ jglue false a =
jglue true a lhs nrefine (_ @@ 1); [nrapply Susp_rec_beta_merid | ].A: Type
a: A
(jglue true a @ (jglue 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 = jglue false a apply concat_1p.
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.