Require Import Classes.interfaces.abstract_algebra.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Cubical.
Require Import Pointed.Core Pointed.pSusp.
Require Import Homotopy.HSpace.Core.
Require Import Homotopy.Suspension.
Require Import Homotopy.Join.Core.

Local Open Scope pointed_scope.
Local Open Scope mc_mult_scope.

(** A Cayley-Dickson Spheroid is a pointed type X which is an H-space, with two operations called negation and conjugation, satisfying the seven following laws.
  --x=x   x**=x   1*=1    (-x)*=-x*   x(-y)=-(xy)   (xy)* = y* x*    x* x=1    *)
Class CayleyDicksonSpheroid (X : pType) := {
  cds_hspace : IsHSpace X;
  cds_negate : Negate X;
  cds_conjug : Conjugate X;
  cds_negate_inv : Involutive cds_negate;
  cds_conjug_inv : Involutive cds_conjug;
  cds_conjug_unit_pres : IsUnitPreserving cds_conjug;
  cds_conjug_left_inv : LeftInverse (.*.) cds_conjug mon_unit;
  cds_conjug_distr : DistrOpp (.*.) cds_conjug;
  cds_swapop : SwapOp (-) cds_conjug;
  cds_factorneg_r : FactorNegRight (-) (.*.);
}.
#[export] Existing Instances
  cds_hspace
  cds_negate
  cds_conjug
  cds_negate_inv
  cds_conjug_inv
  cds_conjug_unit_pres
  cds_conjug_left_inv
  cds_conjug_distr
  cds_swapop
  cds_factorneg_r.

Section CayleyDicksonSpheroid_Properties.

  Context {X : pType} `(CayleyDicksonSpheroid X).

  Global Instance cds_factorneg_l : FactorNegLeft (-) (.*.).
X: pType
H: CayleyDicksonSpheroid X
FactorNegLeft negate sg_op
  Proof.
X: pType
H: CayleyDicksonSpheroid X
FactorNegLeft negate sg_op
    intros x y.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
- x * y = - (x * y)
    transitivity (conj (conj (-x * y))).
X: pType
H: CayleyDicksonSpheroid X
x, y: X
- x * y = conj (conj (- x * y))
X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj (conj (- x * y)) = - (x * y)
    1: symmetry; apply involutive.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj (conj (- x * y)) = - (x * y)
    rewrite distropp.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj (conj y * conj (- x)) = - (x * y)
    rewrite swapop.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj (conj y * - conj x) = - (x * y)
    rewrite factorneg_r.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj (- (conj y * conj x)) = - (x * y)
    rewrite swapop.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
- conj (conj y * conj x) = - (x * y)
    rewrite <- distropp.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
- conj (conj (x * y)) = - (x * y)
    rewrite involutive.
X: pType
H: CayleyDicksonSpheroid X
x, y: X
- (x * y) = - (x * y)
    reflexivity.
  Defined.

  Global Instance cds_conjug_right_inv
    : RightInverse (.*.) cds_conjug mon_unit.
X: pType
H: CayleyDicksonSpheroid X
RightInverse sg_op cds_conjug mon_unit
  Proof.
X: pType
H: CayleyDicksonSpheroid X
RightInverse sg_op cds_conjug mon_unit
    intro x.
X: pType
H: CayleyDicksonSpheroid X
x: X
x * cds_conjug x = mon_unit
    set (p := cds_conjug x).
X: pType
H: CayleyDicksonSpheroid X
x: X
p:= cds_conjug x: X
x * p = mon_unit
    rewrite <- (involutive x).
X: pType
H: CayleyDicksonSpheroid X
x: X
p:= cds_conjug x: X
cds_conjug (cds_conjug x) * p = mon_unit
    apply left_inverse.
  Defined.

End CayleyDicksonSpheroid_Properties.

Global Instance conjugate_susp (A : Type) `(Negate A)
  : Conjugate (Susp A).
A: Type
H: Negate A
Conjugate (Susp A)
Proof.
A: Type
H: Negate A
Conjugate (Susp A)
  srapply Susp_rec.
A: Type
H: Negate A
Susp A
A: Type
H: Negate A
Susp A
A: Type
H: Negate A
A -> ?H_N = ?H_S
  +
A: Type
H: Negate A
Susp A exact North.
  +
A: Type
H: Negate A
Susp A exact South.
  +
A: Type
H: Negate A
A -> North = South intro a.
A: Type
H: Negate A
a: A
North = South
    exact (merid a).
Defined.

Global Instance negate_susp (A : Type) `(Negate A)
  : Negate (Susp A).
A: Type
H: Negate A
Negate (Susp A)
Proof.
A: Type
H: Negate A
Negate (Susp A)
  srapply Susp_rec.
A: Type
H: Negate A
Susp A
A: Type
H: Negate A
Susp A
A: Type
H: Negate A
A -> ?H_N = ?H_S
  +
A: Type
H: Negate A
Susp A exact South.
  +
A: Type
H: Negate A
Susp A exact North.
  +
A: Type
H: Negate A
A -> South = North intro a.
A: Type
H: Negate A
a: A
South = North
    exact (merid (-a))^.
Defined.

Class CayleyDicksonImaginaroid (A : Type) := {
  cdi_negate : Negate A;
  cdi_negate_involutive : Involutive cdi_negate;
  cdi_susp_hspace : IsHSpace (psusp A);
  cdi_susp_factorneg_r : FactorNegRight (negate_susp A cdi_negate) hspace_op;
  cdi_susp_conjug_left_inv : LeftInverse hspace_op (conjugate_susp A cdi_negate) mon_unit;
  cdi_susp_conjug_distr : DistrOpp hspace_op (conjugate_susp A cdi_negate);
}.
#[export] Existing Instances
  cdi_negate
  cdi_negate_involutive
  cdi_susp_hspace
  cdi_susp_factorneg_r
  cdi_susp_conjug_left_inv
  cdi_susp_conjug_distr.

Global Instance involutive_negate_susp {A} `(CayleyDicksonImaginaroid A)
  : Involutive (negate_susp A cdi_negate).
A: Type
H: CayleyDicksonImaginaroid A
Involutive (negate_susp A cdi_negate)
Proof.
A: Type
H: CayleyDicksonImaginaroid A
Involutive (negate_susp A cdi_negate)
  srapply Susp_ind; try reflexivity.
A: Type
H: CayleyDicksonImaginaroid A
forall x : A,
transport
  (fun y : Susp A =>
   negate_susp A cdi_negate
     (negate_susp A cdi_negate y) = y) (merid x)
  1%path = 1%path
  intro x.
A: Type
H: CayleyDicksonImaginaroid A
x: A
transport
  (fun y : Susp A =>
   negate_susp A cdi_negate
     (negate_susp A cdi_negate y) = y) (merid x)
  1%path = 1%path
  apply dp_paths_FFlr.
A: Type
H: CayleyDicksonImaginaroid A
x: A
((ap (negate_susp A cdi_negate)
    (ap (negate_susp A cdi_negate) (merid x)))^ @ 1) @
merid x = 1%path
  rewrite concat_p1.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(ap (negate_susp A cdi_negate)
   (ap (negate_susp A cdi_negate) (merid x)))^ @
merid x = 1%path
  rewrite Susp_rec_beta_merid.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(ap (negate_susp A cdi_negate) (merid (- x))^)^ @
merid x = 1%path
  rewrite ap_V.
A: Type
H: CayleyDicksonImaginaroid A
x: A
((ap (negate_susp A cdi_negate) (merid (- x)))^)^ @
merid x = 1%path
  rewrite Susp_rec_beta_merid.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(((merid (- - x))^)^)^ @ merid x = 1%path
  rewrite inv_V.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(merid (- - x))^ @ merid x = 1%path
  rewrite (involutive x).
A: Type
H: CayleyDicksonImaginaroid A
x: A
(merid x)^ @ merid x = 1%path
  apply concat_Vp.
Defined.

Global Instance involutive_conjugate_susp {A} `(CayleyDicksonImaginaroid A)
  : Involutive (conjugate_susp A cdi_negate).
A: Type
H: CayleyDicksonImaginaroid A
Involutive (conjugate_susp A cdi_negate)
Proof.
A: Type
H: CayleyDicksonImaginaroid A
Involutive (conjugate_susp A cdi_negate)
  srapply Susp_ind; try reflexivity.
A: Type
H: CayleyDicksonImaginaroid A
forall x : A,
transport
  (fun y : Susp A =>
   conjugate_susp A cdi_negate
     (conjugate_susp A cdi_negate y) = y) (merid x)
  1%path = 1%path
  intro x.
A: Type
H: CayleyDicksonImaginaroid A
x: A
transport
  (fun y : Susp A =>
   conjugate_susp A cdi_negate
     (conjugate_susp A cdi_negate y) = y) (merid x)
  1%path = 1%path
  apply dp_paths_FFlr.
A: Type
H: CayleyDicksonImaginaroid A
x: A
((ap (conjugate_susp A cdi_negate)
    (ap (conjugate_susp A cdi_negate) (merid x)))^ @ 1) @
merid x = 1%path
  rewrite concat_p1.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(ap (conjugate_susp A cdi_negate)
   (ap (conjugate_susp A cdi_negate) (merid x)))^ @
merid x = 1%path
  rewrite 2 Susp_rec_beta_merid.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(merid x)^ @ merid x = 1%path
  apply concat_Vp.
Defined.

Global Instance isunitpreserving_conjugate_susp {A} `(CayleyDicksonImaginaroid A)
  : @IsUnitPreserving _ _ pt pt (conjugate_susp A cdi_negate).
A: Type
H: CayleyDicksonImaginaroid A
IsUnitPreserving (conjugate_susp A cdi_negate)
Proof.
A: Type
H: CayleyDicksonImaginaroid A
IsUnitPreserving (conjugate_susp A cdi_negate)
  reflexivity.
Defined.

Global Instance swapop_conjugate_susp {A} `(CayleyDicksonImaginaroid A)
  : SwapOp negate (conjugate_susp A cdi_negate).
A: Type
H: CayleyDicksonImaginaroid A
SwapOp negate (conjugate_susp A cdi_negate)
Proof.
A: Type
H: CayleyDicksonImaginaroid A
SwapOp negate (conjugate_susp A cdi_negate)
  srapply Susp_ind; try reflexivity.
A: Type
H: CayleyDicksonImaginaroid A
forall x : A,
transport (fun y : Susp A => conj (- y) = - conj y)
  (merid x) 1%path = 1%path
  intro x.
A: Type
H: CayleyDicksonImaginaroid A
x: A
transport (fun y : Susp A => conj (- y) = - conj y)
  (merid x) 1%path = 1%path
  apply dp_paths_FlFr.
A: Type
H: CayleyDicksonImaginaroid A
x: A
((ap (fun x : Susp A => conj (- x)) (merid x))^ @ 1) @
ap (fun x : Susp A => - conj x) (merid x) = 1%path
  rewrite concat_p1.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(ap (fun x : Susp A => conj (- x)) (merid x))^ @
ap (fun x : Susp A => - conj x) (merid x) = 1%path
  rewrite ap_compose.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(ap conj (ap negate (merid x)))^ @
ap (fun x : Susp A => - conj x) (merid x) = 1%path
  rewrite (ap_compose negate).
A: Type
H: CayleyDicksonImaginaroid A
x: A
(ap conj (ap negate (merid x)))^ @
ap negate (ap negate (merid x)) = 1%path
  rewrite Susp_rec_beta_merid.
A: Type
H: CayleyDicksonImaginaroid A
x: A
(ap conj (merid (- x))^)^ @
ap negate (ap negate (merid x)) = 1%path
  rewrite ap_V.
A: Type
H: CayleyDicksonImaginaroid A
x: A
((ap conj (merid (- x)))^)^ @
ap negate (ap negate (merid x)) = 1%path
  rewrite inv_V.
A: Type
H: CayleyDicksonImaginaroid A
x: A
ap conj (merid (- x)) @
ap negate (ap negate (merid x)) = 1%path
  rewrite 3 Susp_rec_beta_merid.
A: Type
H: CayleyDicksonImaginaroid A
x: A
merid (- x) @ (merid (- x))^ = 1%path
  apply concat_pV.
Defined.

(** Every suspension of a Cayley-Dickson imaginaroid gives a Cayley-Dickson spheroid. *)
Global Instance cds_susp_cdi {A} `(CayleyDicksonImaginaroid A)
  : CayleyDicksonSpheroid (psusp A) := {}.

Global Instance cdi_conjugate_susp_left_inverse {A} `(CayleyDicksonImaginaroid A)
  : LeftInverse hspace_op (conjugate_susp A cdi_negate) mon_unit.
A: Type
H: CayleyDicksonImaginaroid A
LeftInverse hspace_op (conjugate_susp A cdi_negate)
  mon_unit
Proof.
A: Type
H: CayleyDicksonImaginaroid A
LeftInverse hspace_op (conjugate_susp A cdi_negate)
  mon_unit
  srapply cds_conjug_left_inv.
Defined.

Global Instance cdi_conjugate_susp_right_inverse {A} `(CayleyDicksonImaginaroid A)
  : RightInverse hspace_op (conjugate_susp A cdi_negate) mon_unit.
A: Type
H: CayleyDicksonImaginaroid A
RightInverse hspace_op (conjugate_susp A cdi_negate)
  mon_unit
Proof.
A: Type
H: CayleyDicksonImaginaroid A
RightInverse hspace_op (conjugate_susp A cdi_negate)
  mon_unit
  srapply cds_conjug_right_inv.
Defined.

Global Instance cdi_susp_left_identity {A} `(CayleyDicksonImaginaroid A)
  : LeftIdentity hspace_op mon_unit.
A: Type
H: CayleyDicksonImaginaroid A
LeftIdentity hspace_op mon_unit
Proof.
A: Type
H: CayleyDicksonImaginaroid A
LeftIdentity hspace_op mon_unit
  exact _.
Defined.

Global Instance cdi_susp_right_identity {A} `(CayleyDicksonImaginaroid A)
  : RightIdentity hspace_op mon_unit.
A: Type
H: CayleyDicksonImaginaroid A
RightIdentity hspace_op mon_unit
Proof.
A: Type
H: CayleyDicksonImaginaroid A
RightIdentity hspace_op mon_unit
  exact _.
Defined.

Global Instance cdi_negate_susp_factornegleft {A} `(CayleyDicksonImaginaroid A)
  : FactorNegLeft (negate_susp A cdi_negate) hspace_op.
A: Type
H: CayleyDicksonImaginaroid A
FactorNegLeft (negate_susp A cdi_negate) hspace_op
Proof.
A: Type
H: CayleyDicksonImaginaroid A
FactorNegLeft (negate_susp A cdi_negate) hspace_op
  srapply cds_factorneg_l.
Defined.

(** A Cayley-Dickson imaginaroid A whose multiplciation on the suspension is associative gives rise to a H-space structure on the join of the suspension of A with itself. *)
Section ImaginaroidHSpace.

  (* Let A be a Cayley-Dickson imaginaroid with associative H-space multiplication on Susp A *)
  Context {A} `(CayleyDicksonImaginaroid A)
    `(!Associative hspace_op).

  (** Declaring these as local instances so that they can be found *)
  Local Instance hspace_op' : SgOp (Susp A) := hspace_op.
  Local Instance hspace_unit' : MonUnit (Susp A) := hspace_mon_unit.

  (** First we make some observations with the context we have. *)
  Section Lemmata.

    Context (a b c d : Susp A).

    Local Definition f := (fun x => a * (c * -x)).
    Local Definition g := (fun y => c * (y * b)).

    Lemma lemma1 : f (- mon_unit) = a * c.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
f (- mon_unit) = a * c
    Proof.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
f (- mon_unit) = a * c
      unfold f; apply ap.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * - - mon_unit = c
      exact (hspace_right_identity c).
    Defined.

    Lemma lemma2 : f (conj c * conj a * d * conj b) = (-d) * conj b.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
f (conj c * conj a * d * conj b) = - d * conj b
    Proof.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
f (conj c * conj a * d * conj b) = - d * conj b
      unfold f.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
a * (c * - (conj c * conj a * d * conj b)) =
- d * conj b
      rewrite 2 factorneg_r.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
- (a * (c * (conj c * conj a * d * conj b))) =
- d * conj b
      rewrite 3 simple_associativity.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
- (a * c * (conj c * conj a) * d * conj b) =
- d * conj b
      rewrite <- distropp.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
- (a * c * conj (a * c) * d * conj b) = - d * conj b
      rewrite (right_inverse (a * c)).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
- (mon_unit * d * conj b) = - d * conj b
      rewrite (left_identity d).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
- (d * conj b) = - d * conj b
      symmetry.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
- d * conj b = - (d * conj b)
      apply factorneg_l.
    Defined.

    Lemma lemma3 : g mon_unit = c * b.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
g mon_unit = c * b
    Proof.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
g mon_unit = c * b
      unfold g; apply ap.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
mon_unit * b = b
      apply left_identity.
    Defined.

    Lemma lemma4 : g (conj c * conj a * d * conj b) = conj a * d.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
g (conj c * conj a * d * conj b) = conj a * d
    Proof.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
g (conj c * conj a * d * conj b) = conj a * d
      unfold g.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * (conj c * conj a * d * conj b * b) = conj a * d
      rewrite 2 simple_associativity.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * (conj c * conj a * d) * conj b * b = conj a * d
      rewrite <- simple_associativity.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * (conj c * conj a * d) * (conj b * b) = conj a * d
      rewrite left_inverse.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * (conj c * conj a * d) * mon_unit = conj a * d
      rewrite right_identity.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * (conj c * conj a * d) = conj a * d
      rewrite 2 simple_associativity.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * conj c * conj a * d = conj a * d
      rewrite right_inverse.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
mon_unit * conj a * d = conj a * d
      rewrite <- simple_associativity.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
mon_unit * (conj a * d) = conj a * d
      apply left_identity.
    Defined.

  End Lemmata.

  Arguments f {_ _}.
  Arguments g {_ _}.

  (** Here is the multiplication map in algebraic form:
      (a,b) * (c,d) = (a * c - d * b*, a* * d + c * b)
      the following is the spherical form. *)
  Global Instance cd_op
    : SgOp (pjoin (psusp A) (psusp A)).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
SgOp (pjoin (psusp A) (psusp A))
  Proof.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
SgOp (pjoin (psusp A) (psusp A))
    unfold psusp, pjoin; cbn.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
SgOp (Join (Susp A) (Susp A))
    intros x y; revert x.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
Join (Susp A) (Susp A) -> Join (Susp A) (Susp A)
    srapply Join_rec; hnf.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
Susp A -> Join (Susp A) (Susp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
Susp A -> Join (Susp A) (Susp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
forall a b : Susp A, ?Goal a = ?Goal0 b
    {
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
Susp A -> Join (Susp A) (Susp A) intro a.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
a: Susp A
Join (Susp A) (Susp A)
      revert y.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: Susp A
Join (Susp A) (Susp A) -> Join (Susp A) (Susp A)
      srapply Join_rec; hnf.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: Susp A
Susp A -> Join (Susp A) (Susp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: Susp A
Susp A -> Join (Susp A) (Susp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: Susp A
forall a0 b : Susp A, ?Goal1 a0 = ?Goal2 b
      -
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: Susp A
Susp A -> Join (Susp A) (Susp A) intro c.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, c: Susp A
Join (Susp A) (Susp A)
        exact (joinl (a * c)).
      -
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: Susp A
Susp A -> Join (Susp A) (Susp A) intro d.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, d: Susp A
Join (Susp A) (Susp A)
        exact (joinr (conj a * d)).
      -
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: Susp A
forall a0 b : Susp A,
(fun c : Susp A => joinl (a * c)) a0 =
(fun d : Susp A => joinr (conj a * d)) b intros x y.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, x, y: Susp A
(fun c : Susp A => joinl (a * c)) x =
(fun d : Susp A => joinr (conj a * d)) y
        apply jglue. }
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
Susp A -> Join (Susp A) (Susp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
forall a b : Susp A,
(fun a0 : Susp A =>
 Join_rec
   ((fun c : Susp A => joinl (a0 * c))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun d : Susp A => joinr (conj a0 * d))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun x y : Susp A => jglue (a0 * x) (conj a0 * y))
    :
    forall a1 b0 : Susp A,
    ((fun c : Susp A => joinl (a0 * c))
     :
     Susp A -> Join (Susp A) (Susp A)) a1 =
    ((fun d : Susp A => joinr (conj a0 * d))
     :
     Susp A -> Join (Susp A) (Susp A)) b0) y) a =
?Goal b
    {
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
Susp A -> Join (Susp A) (Susp A) intro b.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
b: Susp A
Join (Susp A) (Susp A)
      revert y.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b: Susp A
Join (Susp A) (Susp A) -> Join (Susp A) (Susp A)
      srapply Join_rec; hnf.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b: Susp A
Susp A -> Join (Susp A) (Susp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b: Susp A
Susp A -> Join (Susp A) (Susp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b: Susp A
forall a b0 : Susp A, ?Goal0 a = ?Goal1 b0
      -
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b: Susp A
Susp A -> Join (Susp A) (Susp A) intro c.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b, c: Susp A
Join (Susp A) (Susp A)
        exact (joinr (c * b)).
      -
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b: Susp A
Susp A -> Join (Susp A) (Susp A) intro d.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b, d: Susp A
Join (Susp A) (Susp A)
        exact (joinl ((-d) * conj b)).
      -
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b: Susp A
forall a b0 : Susp A,
(fun c : Susp A => joinr (c * b)) a =
(fun d : Susp A => joinl (- d * conj b)) b0 intros x y.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b, x, y: Susp A
(fun c : Susp A => joinr (c * b)) x =
(fun d : Susp A => joinl (- d * conj b)) y
        symmetry.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
b, x, y: Susp A
(fun d : Susp A => joinl (- d * conj b)) y =
(fun c : Susp A => joinr (c * b)) x
        apply jglue. }
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
forall a b : Susp A,
(fun a0 : Susp A =>
 Join_rec
   ((fun c : Susp A => joinl (a0 * c))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun d : Susp A => joinr (conj a0 * d))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun x y : Susp A => jglue (a0 * x) (conj a0 * y))
    :
    forall a1 b0 : Susp A,
    ((fun c : Susp A => joinl (a0 * c))
     :
     Susp A -> Join (Susp A) (Susp A)) a1 =
    ((fun d : Susp A => joinr (conj a0 * d))
     :
     Susp A -> Join (Susp A) (Susp A)) b0) y) a =
(fun b0 : Susp A =>
 Join_rec
   ((fun c : Susp A => joinr (c * b0))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun d : Susp A => joinl (- d * conj b0))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun x y : Susp A =>
     (jglue (- y * conj b0) (x * b0))^)
    :
    forall a0 b1 : Susp A,
    ((fun c : Susp A => joinr (c * b0))
     :
     Susp A -> Join (Susp A) (Susp A)) a0 =
    ((fun d : Susp A => joinl (- d * conj b0))
     :
     Susp A -> Join (Susp A) (Susp A)) b1) y) b
    intros a b.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
y: Join (Susp A) (Susp A)
a, b: Susp A
(fun a : Susp A =>
 Join_rec
   ((fun c : Susp A => joinl (a * c))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun d : Susp A => joinr (conj a * d))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun x y : Susp A => jglue (a * x) (conj a * y))
    :
    forall a0 b : Susp A,
    ((fun c : Susp A => joinl (a * c))
     :
     Susp A -> Join (Susp A) (Susp A)) a0 =
    ((fun d : Susp A => joinr (conj a * d))
     :
     Susp A -> Join (Susp A) (Susp A)) b) y) a =
(fun b : Susp A =>
 Join_rec
   ((fun c : Susp A => joinr (c * b))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun d : Susp A => joinl (- d * conj b))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun x y : Susp A =>
     (jglue (- y * conj b) (x * b))^)
    :
    forall a b0 : Susp A,
    ((fun c : Susp A => joinr (c * b))
     :
     Susp A -> Join (Susp A) (Susp A)) a =
    ((fun d : Susp A => joinl (- d * conj b))
     :
     Susp A -> Join (Susp A) (Susp A)) b0) y) b
    revert y.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: Susp A
forall y : Join (Susp A) (Susp A),
(fun a : Susp A =>
 Join_rec
   ((fun c : Susp A => joinl (a * c))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun d : Susp A => joinr (conj a * d))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun x y0 : Susp A => jglue (a * x) (conj a * y0))
    :
    forall a0 b : Susp A,
    ((fun c : Susp A => joinl (a * c))
     :
     Susp A -> Join (Susp A) (Susp A)) a0 =
    ((fun d : Susp A => joinr (conj a * d))
     :
     Susp A -> Join (Susp A) (Susp A)) b) y) a =
(fun b : Susp A =>
 Join_rec
   ((fun c : Susp A => joinr (c * b))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun d : Susp A => joinl (- d * conj b))
    :
    Susp A -> Join (Susp A) (Susp A))
   ((fun x y0 : Susp A =>
     (jglue (- y0 * conj b) (x * b))^)
    :
    forall a b0 : Susp A,
    ((fun c : Susp A => joinr (c * b))
     :
     Susp A -> Join (Susp A) (Susp A)) a =
    ((fun d : Susp A => joinl (- d * conj b))
     :
     Susp A -> Join (Susp A) (Susp A)) b0) y) b
    srapply Join_ind.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: Susp A
forall a0 : Susp A,
(fun x : Join (Susp A) (Susp A) =>
 (fun a : Susp A =>
  Join_rec
    ((fun c : Susp A => joinl (a * c))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun d : Susp A => joinr (conj a * d))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun x0 y : Susp A => jglue (a * x0) (conj a * y))
     :
     forall a1 b : Susp A,
     ((fun c : Susp A => joinl (a * c))
      :
      Susp A -> Join (Susp A) (Susp A)) a1 =
     ((fun d : Susp A => joinr (conj a * d))
      :
      Susp A -> Join (Susp A) (Susp A)) b) x) a =
 (fun b : Susp A =>
  Join_rec
    ((fun c : Susp A => joinr (c * b))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun d : Susp A => joinl (- d * conj b))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun x0 y : Susp A =>
      (jglue (- y * conj b) (x0 * b))^)
     :
     forall a b0 : Susp A,
     ((fun c : Susp A => joinr (c * b))
      :
      Susp A -> Join (Susp A) (Susp A)) a =
     ((fun d : Susp A => joinl (- d * conj b))
      :
      Susp A -> Join (Susp A) (Susp A)) b0) x) b)
  (joinl a0)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: Susp A
forall b0 : Susp A,
(fun x : Join (Susp A) (Susp A) =>
 (fun a : Susp A =>
  Join_rec
    ((fun c : Susp A => joinl (a * c))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun d : Susp A => joinr (conj a * d))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun x0 y : Susp A => jglue (a * x0) (conj a * y))
     :
     forall a0 b : Susp A,
     ((fun c : Susp A => joinl (a * c))
      :
      Susp A -> Join (Susp A) (Susp A)) a0 =
     ((fun d : Susp A => joinr (conj a * d))
      :
      Susp A -> Join (Susp A) (Susp A)) b) x) a =
 (fun b : Susp A =>
  Join_rec
    ((fun c : Susp A => joinr (c * b))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun d : Susp A => joinl (- d * conj b))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun x0 y : Susp A =>
      (jglue (- y * conj b) (x0 * b))^)
     :
     forall a b1 : Susp A,
     ((fun c : Susp A => joinr (c * b))
      :
      Susp A -> Join (Susp A) (Susp A)) a =
     ((fun d : Susp A => joinl (- d * conj b))
      :
      Susp A -> Join (Susp A) (Susp A)) b1) x) b)
  (joinr b0)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: Susp A
forall a0 b0 : Susp A,
transport
  (fun x : Join (Susp A) (Susp A) =>
   (fun a : Susp A =>
    Join_rec
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        jglue (a * x0) (conj a * y))
       :
       forall a1 b : Susp A,
       ((fun c : Susp A => joinl (a * c))
        :
        Susp A -> Join (Susp A) (Susp A)) a1 =
       ((fun d : Susp A => joinr (conj a * d))
        :
        Susp A -> Join (Susp A) (Susp A)) b) x) a =
   (fun b : Susp A =>
    Join_rec
      ((fun c : Susp A => joinr (c * b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinl (- d * conj b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        (jglue (- y * conj b) (x0 * b))^)
       :
       forall a b1 : Susp A,
       ((fun c : Susp A => joinr (c * b))
        :
        Susp A -> Join (Susp A) (Susp A)) a =
       ((fun d : Susp A => joinl (- d * conj b))
        :
        Susp A -> Join (Susp A) (Susp A)) b1) x) b)
  (jglue a0 b0) (?P_A a0) = 
?P_B b0
    1: intro; apply jglue.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: Susp A
forall b0 : Susp A,
(fun x : Join (Susp A) (Susp A) =>
 (fun a : Susp A =>
  Join_rec
    ((fun c : Susp A => joinl (a * c))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun d : Susp A => joinr (conj a * d))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun x0 y : Susp A => jglue (a * x0) (conj a * y))
     :
     forall a0 b : Susp A,
     ((fun c : Susp A => joinl (a * c))
      :
      Susp A -> Join (Susp A) (Susp A)) a0 =
     ((fun d : Susp A => joinr (conj a * d))
      :
      Susp A -> Join (Susp A) (Susp A)) b) x) a =
 (fun b : Susp A =>
  Join_rec
    ((fun c : Susp A => joinr (c * b))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun d : Susp A => joinl (- d * conj b))
     :
     Susp A -> Join (Susp A) (Susp A))
    ((fun x0 y : Susp A =>
      (jglue (- y * conj b) (x0 * b))^)
     :
     forall a b1 : Susp A,
     ((fun c : Susp A => joinr (c * b))
      :
      Susp A -> Join (Susp A) (Susp A)) a =
     ((fun d : Susp A => joinl (- d * conj b))
      :
      Susp A -> Join (Susp A) (Susp A)) b1) x) b)
  (joinr b0)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: Susp A
forall a0 b0 : Susp A,
transport
  (fun x : Join (Susp A) (Susp A) =>
   (fun a : Susp A =>
    Join_rec
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        jglue (a * x0) (conj a * y))
       :
       forall a1 b : Susp A,
       ((fun c : Susp A => joinl (a * c))
        :
        Susp A -> Join (Susp A) (Susp A)) a1 =
       ((fun d : Susp A => joinr (conj a * d))
        :
        Susp A -> Join (Susp A) (Susp A)) b) x) a =
   (fun b : Susp A =>
    Join_rec
      ((fun c : Susp A => joinr (c * b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinl (- d * conj b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        (jglue (- y * conj b) (x0 * b))^)
       :
       forall a b1 : Susp A,
       ((fun c : Susp A => joinr (c * b))
        :
        Susp A -> Join (Susp A) (Susp A)) a =
       ((fun d : Susp A => joinl (- d * conj b))
        :
        Susp A -> Join (Susp A) (Susp A)) b1) x) b)
  (jglue a0 b0)
  ((fun a1 : Susp A => jglue (a * a1) (a1 * b)) a0) =
?P_B b0
    1: intro; cbn; symmetry; apply jglue.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: Susp A
forall a0 b0 : Susp A,
transport
  (fun x : Join (Susp A) (Susp A) =>
   (fun a : Susp A =>
    Join_rec
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        jglue (a * x0) (conj a * y))
       :
       forall a1 b : Susp A,
       ((fun c : Susp A => joinl (a * c))
        :
        Susp A -> Join (Susp A) (Susp A)) a1 =
       ((fun d : Susp A => joinr (conj a * d))
        :
        Susp A -> Join (Susp A) (Susp A)) b) x) a =
   (fun b : Susp A =>
    Join_rec
      ((fun c : Susp A => joinr (c * b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinl (- d * conj b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        (jglue (- y * conj b) (x0 * b))^)
       :
       forall a b1 : Susp A,
       ((fun c : Susp A => joinr (c * b))
        :
        Susp A -> Join (Susp A) (Susp A)) a =
       ((fun d : Susp A => joinl (- d * conj b))
        :
        Susp A -> Join (Susp A) (Susp A)) b1) x) b)
  (jglue a0 b0)
  ((fun a1 : Susp A => jglue (a * a1) (a1 * b)) a0) =
(fun b1 : Susp A =>
 (jglue (- b1 * conj b) (conj a * b1))^
 :
 (fun x : Join (Susp A) (Susp A) =>
  (fun a : Susp A =>
   Join_rec
     ((fun c : Susp A => joinl (a * c))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun d : Susp A => joinr (conj a * d))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun x0 y : Susp A =>
       jglue (a * x0) (conj a * y))
      :
      forall a1 b : Susp A,
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A)) a1 =
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A)) b) x) a =
  (fun b : Susp A =>
   Join_rec
     ((fun c : Susp A => joinr (c * b))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun d : Susp A => joinl (- d * conj b))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun x0 y : Susp A =>
       (jglue (- y * conj b) (x0 * b))^)
      :
      forall a b2 : Susp A,
      ((fun c : Susp A => joinr (c * b))
       :
       Susp A -> Join (Susp A) (Susp A)) a =
      ((fun d : Susp A => joinl (- d * conj b))
       :
       Susp A -> Join (Susp A) (Susp A)) b2) x) b)
   (joinr b1)) b0
    intros c d.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
transport
  (fun x : Join (Susp A) (Susp A) =>
   (fun a : Susp A =>
    Join_rec
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        jglue (a * x0) (conj a * y))
       :
       forall a0 b : Susp A,
       ((fun c : Susp A => joinl (a * c))
        :
        Susp A -> Join (Susp A) (Susp A)) a0 =
       ((fun d : Susp A => joinr (conj a * d))
        :
        Susp A -> Join (Susp A) (Susp A)) b) x) a =
   (fun b : Susp A =>
    Join_rec
      ((fun c : Susp A => joinr (c * b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinl (- d * conj b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x0 y : Susp A =>
        (jglue (- y * conj b) (x0 * b))^)
       :
       forall a b0 : Susp A,
       ((fun c : Susp A => joinr (c * b))
        :
        Susp A -> Join (Susp A) (Susp A)) a =
       ((fun d : Susp A => joinl (- d * conj b))
        :
        Susp A -> Join (Susp A) (Susp A)) b0) x) b)
  (jglue c d)
  ((fun a0 : Susp A => jglue (a * a0) (a0 * b)) c) =
(fun b0 : Susp A =>
 (jglue (- b0 * conj b) (conj a * b0))^
 :
 (fun x : Join (Susp A) (Susp A) =>
  (fun a : Susp A =>
   Join_rec
     ((fun c : Susp A => joinl (a * c))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun d : Susp A => joinr (conj a * d))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun x0 y : Susp A =>
       jglue (a * x0) (conj a * y))
      :
      forall a0 b : Susp A,
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A)) a0 =
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A)) b) x) a =
  (fun b : Susp A =>
   Join_rec
     ((fun c : Susp A => joinr (c * b))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun d : Susp A => joinl (- d * conj b))
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun x0 y : Susp A =>
       (jglue (- y * conj b) (x0 * b))^)
      :
      forall a b1 : Susp A,
      ((fun c : Susp A => joinr (c * b))
       :
       Susp A -> Join (Susp A) (Susp A)) a =
      ((fun d : Susp A => joinl (- d * conj b))
       :
       Susp A -> Join (Susp A) (Susp A)) b1) x) b)
   (joinr b0)) d
    apply sq_dp^-1.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare (jglue (a * c) (c * b))
  (jglue (- d * conj b) (conj a * d))^
  (ap
     (fun x : Join (Susp A) (Susp A) =>
      Join_rec (fun c : Susp A => joinl (a * c))
        (fun d : Susp A => joinr (conj a * d))
        (fun x0 y : Susp A =>
         jglue (a * x0) (conj a * y)) x) (jglue c d))
  (ap
     (fun x : Join (Susp A) (Susp A) =>
      Join_rec (fun c : Susp A => joinr (c * b))
        (fun d : Susp A => joinl (- d * conj b))
        (fun x0 y : Susp A =>
         (jglue (- y * conj b) (x0 * b))^) x)
     (jglue c d))
    refine (sq_ccGG _^ _^ _).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
ap
  (fun x : Join (Susp A) (Susp A) =>
   Join_rec (fun c : Susp A => joinl (a * c))
     (fun d : Susp A => joinr (conj a * d))
     (fun x0 y : Susp A => jglue (a * x0) (conj a * y))
     x) (jglue c d) = ?Goal
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
ap
  (fun x : Join (Susp A) (Susp A) =>
   Join_rec (fun c : Susp A => joinr (c * b))
     (fun d : Susp A => joinl (- d * conj b))
     (fun x0 y : Susp A =>
      (jglue (- y * conj b) (x0 * b))^) x) 
  (jglue c d) = ?Goal0
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare (jglue (a * c) (c * b))
  (jglue (- d * conj b) (conj a * d))^ 
  ?Goal ?Goal0
    1,2: apply Join_rec_beta_jglue.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare (jglue (a * c) (c * b))
  (jglue (- d * conj b) (conj a * d))^
  (jglue (a * c) (conj a * d))
  (jglue (- d * conj b) (c * b))^
    change (PathSquare (jglue (a * c) (c * b)) (jglue ((- d) * conj b) (conj a * d))^
      (jglue (a * c) (conj a * d)) (jglue ((- d) * conj b) (c * b))^).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare (jglue (a * c) (c * b))
  (jglue (- d * conj b) (conj a * d))^
  (jglue (a * c) (conj a * d))
  (jglue (- d * conj b) (c * b))^
    rewrite <- (lemma1 a c), <- (lemma2 a b c d),
       <- (lemma3 b c), <- (lemma4 a b c d).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare (jglue (f (- mon_unit)) (g mon_unit))
  (jglue (f (conj c * conj a * d * conj b))
     (g (conj c * conj a * d * conj b)))^
  (jglue (f (- mon_unit))
     (g (conj c * conj a * d * conj b)))
  (jglue (f (conj c * conj a * d * conj b))
     (g mon_unit))^
    refine (sq_GGGG _ _ _ _ _).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal = jglue (f (- mon_unit)) (g mon_unit)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal0 =
(jglue (f (conj c * conj a * d * conj b))
   (g (conj c * conj a * d * conj b)))^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal1 =
jglue (f (- mon_unit))
  (g (conj c * conj a * d * conj b))
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal2 =
(jglue (f (conj c * conj a * d * conj b)) (g mon_unit))^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare ?Goal ?Goal0 ?Goal1 ?Goal2
    2,4: apply ap.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal = jglue (f (- mon_unit)) (g mon_unit)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?x =
jglue (f (conj c * conj a * d * conj b))
  (g (conj c * conj a * d * conj b))
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?x0 =
jglue (f (conj c * conj a * d * conj b)) (g mon_unit)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal0 =
jglue (f (- mon_unit))
  (g (conj c * conj a * d * conj b))
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare ?Goal ?x^ ?Goal0 ?x0^
    1,2,3,4: srapply (Join_rec_beta_jglue _ _ (fun a b => jglue (f a) (g b))).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (- mon_unit) mon_unit))
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (conj c * conj a * d * conj b)
        (conj c * conj a * d * conj b)))^
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (- mon_unit)
        (conj c * conj a * d * conj b)))
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (conj c * conj a * d * conj b) mon_unit))^
    refine (sq_cGcG _ _ _).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal =
(ap
   (Join_rec (fun a0 : Susp A => joinl (f a0))
      (fun b0 : Susp A => joinr (g b0))
      (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
   (jglue (conj c * conj a * d * conj b)
      (conj c * conj a * d * conj b)))^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
?Goal0 =
(ap
   (Join_rec (fun a0 : Susp A => joinl (f a0))
      (fun b0 : Susp A => joinr (g b0))
      (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
   (jglue (conj c * conj a * d * conj b) mon_unit))^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (- mon_unit) mon_unit)) 
  ?Goal
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (- mon_unit)
        (conj c * conj a * d * conj b))) 
  ?Goal0
    1,2: exact (ap_V _ (jglue _ _ )).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (- mon_unit) mon_unit))
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (conj c * conj a * d * conj b)
        (conj c * conj a * d * conj b))^)
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (- mon_unit)
        (conj c * conj a * d * conj b)))
  (ap
     (Join_rec (fun a0 : Susp A => joinl (f a0))
        (fun b0 : Susp A => joinr (g b0))
        (fun a0 b0 : Susp A => jglue (f a0) (g b0)))
     (jglue (conj c * conj a * d * conj b) mon_unit)^)
    refine (@sq_ap _ _ _ _ _ _ _ (jglue _ _) (jglue _ _)^
      (jglue _ _) (jglue _ _)^ _).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
PathSquare (jglue (- mon_unit) mon_unit)
  (jglue (conj c * conj a * d * conj b)
     (conj c * conj a * d * conj b))^
  (jglue (- mon_unit) (conj c * conj a * d * conj b))
  (jglue (conj c * conj a * d * conj b) mon_unit)^
    generalize (conj c * conj a * d * conj b).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
forall s : Susp A,
PathSquare (jglue (- mon_unit) mon_unit) (jglue s s)^
  (jglue (- mon_unit) s) (jglue s mon_unit)^
    clear a b c d.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall s : Susp A,
PathSquare (jglue (- mon_unit) mon_unit) (jglue s s)^
  (jglue (- mon_unit) s) (jglue s mon_unit)^
    change (forall s : Susp A,
      Diamond (-mon_unit) s (mon_unit) s).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall s : Susp A, Diamond (- mon_unit) s mon_unit s
    srapply Susp_ind; hnf.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
PathSquare (jglue (- mon_unit) mon_unit)
  (jglue North North)^ (jglue (- mon_unit) North)
  (jglue North mon_unit)^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
PathSquare (jglue (- mon_unit) mon_unit)
  (jglue South South)^ 
  (jglue (- mon_unit) South) 
  (jglue South mon_unit)^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall x : A,
transport
  (fun y : Susp A => Diamond (- mon_unit) y mon_unit y)
  (merid x) ?Goal = ?Goal0
    1: by apply diamond_v_sq.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
PathSquare (jglue (- mon_unit) mon_unit)
  (jglue South South)^ (jglue (- mon_unit) South)
  (jglue South mon_unit)^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall x : A,
transport
  (fun y : Susp A => Diamond (- mon_unit) y mon_unit y)
  (merid x) (diamond_v_sq (- mon_unit) North 1) =
?Goal
    1: by apply diamond_h_sq.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall x : A,
transport
  (fun y : Susp A => Diamond (- mon_unit) y mon_unit y)
  (merid x) (diamond_v_sq (- mon_unit) North 1) =
diamond_h_sq mon_unit South 1
    intro a.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: A
transport
  (fun y : Susp A => Diamond (- mon_unit) y mon_unit y)
  (merid a) (diamond_v_sq (- mon_unit) North 1) =
diamond_h_sq mon_unit South 1
    apply diamond_twist.
  Defined.

  Global Instance cd_op_left_identity
    : LeftIdentity cd_op pt.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
LeftIdentity cd_op pt
  Proof.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
LeftIdentity cd_op pt
    snrapply Join_ind_FFlr.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a : psusp A,
cd_op pt (idmap (joinl a)) = joinl a
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall b : psusp A,
cd_op pt (idmap (joinr b)) = joinr b
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap (cd_op pt) (ap idmap (jglue a b)) @ ?Hr b =
?Hl a @ jglue a b
    1,2: exact (fun _ => ap _ (hspace_left_identity _)).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap (cd_op pt) (ap idmap (jglue a b)) @
(fun b0 : psusp A =>
 ap joinr (hspace_left_identity b0)) b =
(fun a0 : psusp A =>
 ap joinl (hspace_left_identity a0)) a @ jglue a b
    intros a b.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap (cd_op pt) (ap idmap (jglue a b)) @
(fun b : psusp A => ap joinr (hspace_left_identity b))
  b =
(fun a : psusp A => ap joinl (hspace_left_identity a))
  a @ jglue a b
    lhs nrapply whiskerR.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap (cd_op pt) (ap idmap (jglue a b)) = ?Goal
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
?Goal @ ap joinr (hspace_left_identity b) =
ap joinl (hspace_left_identity a) @ jglue a b
    {
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap (cd_op pt) (ap idmap (jglue a b)) = ?Goal lhs refine (ap _ (ap_idmap _)).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap (cd_op pt) (jglue a b) = ?Goal
      exact (Join_rec_beta_jglue
        (fun c => joinl (pt * c))
        (fun d => joinr (conj pt * d))
        (fun x y => jglue (pt * x) (conj pt * y))
        a b). }
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
jglue (pt * a) (conj pt * b) @
ap joinr (hspace_left_identity b) =
ap joinl (hspace_left_identity a) @ jglue a b
    symmetry.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap joinl (hspace_left_identity a) @ jglue a b =
jglue (pt * a) (conj pt * b) @
ap joinr (hspace_left_identity b)
    apply join_natsq.
  Defined.

  Global Instance cd_op_right_identity
    : RightIdentity cd_op pt.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
RightIdentity cd_op pt
  Proof.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
RightIdentity cd_op pt
    snrapply Join_ind_FFlr.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a : psusp A,
Join_rec
  ((fun a0 : Susp A =>
    Join_rec
      ((fun c : Susp A => joinl (a0 * c))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinr (conj a0 * d))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x y : Susp A =>
        jglue (a0 * x) (conj a0 * y))
       :
       forall a1 b : Susp A,
       ((fun c : Susp A => joinl (a0 * c))
        :
        Susp A -> Join (Susp A) (Susp A)) a1 =
       ((fun d : Susp A => joinr (conj a0 * d))
        :
        Susp A -> Join (Susp A) (Susp A)) b) pt)
   :
   Susp A -> Join (Susp A) (Susp A))
  ((fun b : Susp A =>
    Join_rec
      ((fun c : Susp A => joinr (c * b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinl (- d * conj b))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x y : Susp A =>
        (jglue (- y * conj b) (x * b))^)
       :
       forall a0 b0 : Susp A,
       ((fun c : Susp A => joinr (c * b))
        :
        Susp A -> Join (Susp A) (Susp A)) a0 =
       ((fun d : Susp A => joinl (- d * conj b))
        :
        Susp A -> Join (Susp A) (Susp A)) b0) pt)
   :
   Susp A -> Join (Susp A) (Susp A))
  ((fun a0 b : Susp A =>
    Join_ind
      (fun x : Join (Susp A) (Susp A) =>
       (fun a1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinl (a1 * c))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinr (conj a1 * d))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x0 y : Susp A =>
            jglue (a1 * x0) (conj a1 * y))
           :
           forall a2 b0 : Susp A,
           ((fun c : Susp A => joinl (a1 * c))
            :
            Susp A -> Join (Susp A) (Susp A)) a2 =
           ((fun d : Susp A => joinr (... * d))
            :
            Susp A -> Join (Susp A) (Susp A)) b0) x)
         a0 =
       (fun b0 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinr (c * b0))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinl (- d * conj b0))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x0 y : Susp A =>
            (jglue (- y * conj b0) (x0 * b0))^)
           :
           forall a1 b1 : Susp A,
           ((fun c : Susp A => joinr (c * b0))
            :
            Susp A -> Join (Susp A) (Susp A)) a1 =
           ((fun d : Susp A => joinl (... * ...))
            :
            Susp A -> Join (Susp A) (Susp A)) b1) x) b)
      (fun a1 : Susp A => jglue (a0 * a1) (a1 * b))
      (fun b0 : Susp A =>
       (jglue (- b0 * conj b) (conj a0 * b0))^
       :
       (fun x : Join (Susp A) (Susp A) =>
        (fun a1 : Susp A =>
         Join_rec
           ((fun c : Susp A => joinl (a1 * c))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun d : Susp A => joinr (conj a1 * d))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun x0 y : Susp A =>
             jglue (a1 * x0) (conj a1 * y))
            :
            forall a2 b1 : Susp A,
            ((...) : ... -> ...) a2 =
            ((...) : ... -> ...) b1) x) a0 =
        (fun b1 : Susp A =>
         Join_rec
           ((fun c : Susp A => joinr (c * b1))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun d : Susp A => joinl (- d * conj b1))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun x0 y : Susp A =>
             (jglue (... * ...) (x0 * b1))^)
            :
            forall a1 b2 : Susp A,
            ((...) : ... -> ...) a1 =
            ((...) : ... -> ...) b2) x) b) (joinr b0))
      (fun c d : Susp A =>
       sq_dp^-1
         (sq_ccGG
            (Join_rec_beta_jglue
               (fun c0 : Susp A => joinl (a0 * c0))
               (fun d0 : Susp A =>
                joinr (conj a0 * d0))
               (fun x y : Susp A =>
                jglue (a0 * x) (conj a0 * y)) c d)^
            (Join_rec_beta_jglue
               (fun c0 : Susp A => joinr (c0 * b))
               (fun d0 : Susp A =>
                joinl (- d0 * conj b))
               (fun x y : Susp A =>
                (jglue (- y * conj b) (x * b))^) c d)^
            (internal_paths_rew
               (fun s : Susp A =>
                PathSquare (jglue s (c * b))
                  (jglue (- d * conj b) (conj a0 * d))^
                  (jglue s (conj a0 * d))
                  (jglue (- d * conj b) (c * b))^)
               (internal_paths_rew
                  (fun s : Susp A =>
                   PathSquare
                     (jglue (f (- mon_unit)) (c * b))
                     (jglue s (conj a0 * d))^
                     (jglue (f (- mon_unit))
                        (conj a0 * d))
                     (jglue s (c * b))^)
                  (internal_paths_rew
                     (fun s : Susp A =>
                      PathSquare (jglue (f (...)) s)
                        (jglue (f (...)) (conj a0 * d))^
                        (jglue (f (...)) (conj a0 * d))
                        (jglue (f (...)) s)^)
                     (internal_paths_rew
                        (fun s : Susp A =>
                         PathSquare
                           (jglue (...) (...))
                           (jglue (...) s)^
                           (jglue (...) s)
                           (jglue (...) (...))^)
                        (sq_GGGG
                           (Join_rec_beta_jglue
                              (... => ...)
                              (... => ...)
                              (... => ...)
                              (- mon_unit) mon_unit)
                           (ap inverse
                              (Join_rec_beta_jglue ...
                                 ... ... ... ...))
                           (Join_rec_beta_jglue
                              (... => ...)
                              (... => ...)
                              (... => ...)
                              (- mon_unit) (... * ...))
                           (ap inverse
                              (Join_rec_beta_jglue ...
                                 ... ... ... mon_unit))
                           (sq_cGcG (ap_V ... ...)
                              (ap_V ... ...)
                              (sq_ap ... ...)))
                        (lemma4 a0 b c d))
                     (lemma3 b c)) (lemma2 a0 b c d))
               (lemma1 a0 c)))) pt)
   :
   forall a0 b : Susp A,
   ((fun a1 : Susp A =>
     Join_rec
       ((fun c : Susp A => joinl (a1 * c))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun d : Susp A => joinr (conj a1 * d))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun x y : Susp A =>
         jglue (a1 * x) (conj a1 * y))
        :
        forall a2 b0 : Susp A,
        ((fun c : Susp A => joinl (a1 * c))
         :
         Susp A -> Join (Susp A) (Susp A)) a2 =
        ((fun d : Susp A => joinr (conj a1 * d))
         :
         Susp A -> Join (Susp A) (Susp A)) b0) pt)
    :
    Susp A -> Join (Susp A) (Susp A)) a0 =
   ((fun b0 : Susp A =>
     Join_rec
       ((fun c : Susp A => joinr (c * b0))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun d : Susp A => joinl (- d * conj b0))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun x y : Susp A =>
         (jglue (- y * conj b0) (x * b0))^)
        :
        forall a1 b1 : Susp A,
        ((fun c : Susp A => joinr (c * b0))
         :
         Susp A -> Join (Susp A) (Susp A)) a1 =
        ((fun d : Susp A => joinl (- d * conj b0))
         :
         Susp A -> Join (Susp A) (Susp A)) b1) pt)
    :
    Susp A -> Join (Susp A) (Susp A)) b)
  (idmap (joinl a)) = joinl a
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall b : psusp A,
Join_rec
  ((fun a : Susp A =>
    Join_rec
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x y : Susp A => jglue (a * x) (conj a * y))
       :
       forall a0 b0 : Susp A,
       ((fun c : Susp A => joinl (a * c))
        :
        Susp A -> Join (Susp A) (Susp A)) a0 =
       ((fun d : Susp A => joinr (conj a * d))
        :
        Susp A -> Join (Susp A) (Susp A)) b0) pt)
   :
   Susp A -> Join (Susp A) (Susp A))
  ((fun b0 : Susp A =>
    Join_rec
      ((fun c : Susp A => joinr (c * b0))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinl (- d * conj b0))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x y : Susp A =>
        (jglue (- y * conj b0) (x * b0))^)
       :
       forall a b1 : Susp A,
       ((fun c : Susp A => joinr (c * b0))
        :
        Susp A -> Join (Susp A) (Susp A)) a =
       ((fun d : Susp A => joinl (- d * conj b0))
        :
        Susp A -> Join (Susp A) (Susp A)) b1) pt)
   :
   Susp A -> Join (Susp A) (Susp A))
  ((fun a b0 : Susp A =>
    Join_ind
      (fun x : Join (Susp A) (Susp A) =>
       (fun a0 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinl (a0 * c))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinr (conj a0 * d))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x0 y : Susp A =>
            jglue (a0 * x0) (conj a0 * y))
           :
           forall a1 b1 : Susp A,
           ((fun c : Susp A => joinl (a0 * c))
            :
            Susp A -> Join (Susp A) (Susp A)) a1 =
           ((fun d : Susp A => joinr (... * d))
            :
            Susp A -> Join (Susp A) (Susp A)) b1) x) a =
       (fun b1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinr (c * b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinl (- d * conj b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x0 y : Susp A =>
            (jglue (- y * conj b1) (x0 * b1))^)
           :
           forall a0 b2 : Susp A,
           ((fun c : Susp A => joinr (c * b1))
            :
            Susp A -> Join (Susp A) (Susp A)) a0 =
           ((fun d : Susp A => joinl (... * ...))
            :
            Susp A -> Join (Susp A) (Susp A)) b2) x)
         b0)
      (fun a0 : Susp A => jglue (a * a0) (a0 * b0))
      (fun b1 : Susp A =>
       (jglue (- b1 * conj b0) (conj a * b1))^
       :
       (fun x : Join (Susp A) (Susp A) =>
        (fun a0 : Susp A =>
         Join_rec
           ((fun c : Susp A => joinl (a0 * c))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun d : Susp A => joinr (conj a0 * d))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun x0 y : Susp A =>
             jglue (a0 * x0) (conj a0 * y))
            :
            forall a1 b2 : Susp A,
            ((...) : ... -> ...) a1 =
            ((...) : ... -> ...) b2) x) a =
        (fun b2 : Susp A =>
         Join_rec
           ((fun c : Susp A => joinr (c * b2))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun d : Susp A => joinl (- d * conj b2))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun x0 y : Susp A =>
             (jglue (... * ...) (x0 * b2))^)
            :
            forall a0 b3 : Susp A,
            ((...) : ... -> ...) a0 =
            ((...) : ... -> ...) b3) x) b0) 
         (joinr b1))
      (fun c d : Susp A =>
       sq_dp^-1
         (sq_ccGG
            (Join_rec_beta_jglue
               (fun c0 : Susp A => joinl (a * c0))
               (fun d0 : Susp A => joinr (conj a * d0))
               (fun x y : Susp A =>
                jglue (a * x) (conj a * y)) c d)^
            (Join_rec_beta_jglue
               (fun c0 : Susp A => joinr (c0 * b0))
               (fun d0 : Susp A =>
                joinl (- d0 * conj b0))
               (fun x y : Susp A =>
                (jglue (- y * conj b0) (x * b0))^) c d)^
            (internal_paths_rew
               (fun s : Susp A =>
                PathSquare 
                  (jglue s (c * b0))
                  (jglue (- d * conj b0) (conj a * d))^
                  (jglue s (conj a * d))
                  (jglue (- d * conj b0) (c * b0))^)
               (internal_paths_rew
                  (fun s : Susp A =>
                   PathSquare
                    (jglue (f (- mon_unit)) (c * b0))
                    (jglue s (conj a * d))^
                    (jglue 
                    (f (- mon_unit)) 
                    (conj a * d)) 
                    (jglue s (c * b0))^)
                  (internal_paths_rew
                    (fun s : Susp A =>
                    PathSquare 
                    (jglue (f (...)) s)
                    (jglue (f (...)) (conj a * d))^
                    (jglue (f (...)) (conj a * d))
                    (jglue (f (...)) s)^)
                    (internal_paths_rew
                    (fun s : Susp A =>
                    PathSquare 
                    (jglue (...) (...))
                    (jglue (...) s)^ 
                    (jglue (...) s)
                    (jglue (...) (...))^)
                    (sq_GGGG
                    (Join_rec_beta_jglue 
                    (... => ...) 
                    (... => ...) 
                    (... => ...) 
                    (- mon_unit) mon_unit)
                    (ap inverse
                    (Join_rec_beta_jglue ... ... ...
                    ... ...))
                    (Join_rec_beta_jglue 
                    (... => ...) 
                    (... => ...) 
                    (... => ...) 
                    (- mon_unit) 
                    (... * ...))
                    (ap inverse
                    (Join_rec_beta_jglue ... ... ...
                    ... mon_unit))
                    (sq_cGcG 
                    (ap_V ... ...) 
                    (ap_V ... ...) 
                    (sq_ap ... ...)))
                    (lemma4 a b0 c d)) 
                    (lemma3 b0 c)) 
                  (lemma2 a b0 c d)) 
               (lemma1 a c)))) pt)
   :
   forall a b0 : Susp A,
   ((fun a0 : Susp A =>
     Join_rec
       ((fun c : Susp A => joinl (a0 * c))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun d : Susp A => joinr (conj a0 * d))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun x y : Susp A =>
         jglue (a0 * x) (conj a0 * y))
        :
        forall a1 b1 : Susp A,
        ((fun c : Susp A => joinl (a0 * c))
         :
         Susp A -> Join (Susp A) (Susp A)) a1 =
        ((fun d : Susp A => joinr (conj a0 * d))
         :
         Susp A -> Join (Susp A) (Susp A)) b1) pt)
    :
    Susp A -> Join (Susp A) (Susp A)) a =
   ((fun b1 : Susp A =>
     Join_rec
       ((fun c : Susp A => joinr (c * b1))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun d : Susp A => joinl (- d * conj b1))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun x y : Susp A =>
         (jglue (- y * conj b1) (x * b1))^)
        :
        forall a0 b2 : Susp A,
        ((fun c : Susp A => joinr (c * b1))
         :
         Susp A -> Join (Susp A) (Susp A)) a0 =
        ((fun d : Susp A => joinl (- d * conj b1))
         :
         Susp A -> Join (Susp A) (Susp A)) b2) pt)
    :
    Susp A -> Join (Susp A) (Susp A)) b0)
  (idmap (joinr b)) = 
joinr b
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap
  (Join_rec
     ((fun a0 : Susp A =>
       Join_rec
         ((fun c : Susp A => joinl (a0 * c))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinr (conj a0 * d))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           jglue (a0 * x) (conj a0 * y))
          :
          forall a1 b0 : Susp A,
          ((fun c : Susp A => joinl (a0 * c))
           :
           Susp A -> Join (Susp A) (Susp A)) a1 =
          ((fun d : Susp A => joinr (conj a0 * d))
           :
           Susp A -> Join (Susp A) (Susp A)) b0) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun b0 : Susp A =>
       Join_rec
         ((fun c : Susp A => joinr (c * b0))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinl (- d * conj b0))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           (jglue (- y * conj b0) (x * b0))^)
          :
          forall a0 b1 : Susp A,
          ((fun c : Susp A => joinr (c * b0))
           :
           Susp A -> Join (Susp A) (Susp A)) a0 =
          ((fun d : Susp A => joinl (- d * conj b0))
           :
           Susp A -> Join (Susp A) (Susp A)) b1) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun a0 b0 : Susp A =>
       Join_ind
         (fun x : Join (Susp A) (Susp A) =>
          (fun a1 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinl (a1 * c))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinr (conj a1 * d))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               jglue (a1 * x0) (conj a1 * y))
              :
              forall 
              a2 b1 : Susp A,
              ((... => ...) : Susp A -> Join ... ...)
                a2 =
              ((... => ...) : Susp A -> Join ... ...)
                b1) x) a0 =
          (fun b1 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinr (c * b1))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinl (- d * conj b1))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               (jglue (- y * conj b1) (x0 * b1))^)
              :
              forall 
              a1 b2 : Susp A,
              ((... => ...) : Susp A -> Join ... ...)
                a1 =
              ((... => ...) : Susp A -> Join ... ...)
                b2) x) b0)
         (fun a1 : Susp A => jglue (a0 * a1) (a1 * b0))
         (fun b1 : Susp A =>
          (jglue (- b1 * conj b0) (conj a0 * b1))^
          :
          (fun x : Join (Susp A) (Susp A) =>
           (fun a1 : Susp A =>
            Join_rec
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => jglue ... ...)
               :
               forall a2 b2 : Susp A, ... a2 = ... b2)
              x) a0 =
           (fun b2 : Susp A =>
            Join_rec
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => (...)^)
               :
               forall a1 b3 : Susp A, ... a1 = ... b3)
              x) b0) 
            (joinr b1))
         (fun c d : Susp A =>
          sq_dp^-1
            (sq_ccGG
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinl (a0 * c0))
                  (fun d0 : Susp A =>
                   joinr (conj a0 * d0))
                  (fun x y : Susp A =>
                   jglue (a0 * x) (conj a0 * y)) c d)^
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinr (c0 * b0))
                  (fun d0 : Susp A =>
                   joinl (- d0 * conj b0))
                  (fun x y : Susp A =>
                   (jglue (- y * conj b0) (x * b0))^)
                  c d)^
               (internal_paths_rew
                  (fun s : Susp A =>
                   PathSquare 
                    (jglue s (c * b0))
                    (jglue 
                    (- d * conj b0) 
                    (conj a0 * d))^
                    (jglue s (conj a0 * d))
                    (jglue (- d * conj b0) (c * b0))^)
                  (internal_paths_rew
                    (fun s : Susp A =>
                    PathSquare
                    (jglue (f ...) (c * b0))
                    (jglue s (... * d))^
                    (jglue (f ...) (... * d))
                    (jglue s (c * b0))^)
                    (internal_paths_rew
                    (fun s : Susp A =>
                    PathSquare 
                    (jglue ... s) 
                    (jglue ... ...)^ 
                    (jglue ... ...) 
                    (jglue ... s)^)
                    (internal_paths_rew
                    (fun ... =>
                    PathSquare ... ...^ ... ...^)
                    (sq_GGGG 
                    (...) 
                    (...) 
                    (...) 
                    (...) 
                    (...)) 
                    (lemma4 a0 b0 c d)) 
                    (lemma3 b0 c)) 
                    (lemma2 a0 b0 c d)) 
                  (lemma1 a0 c)))) pt)
      :
      forall a0 b0 : Susp A,
      ((fun a1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinl (a1 * c))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinr (conj a1 * d))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            jglue (a1 * x) (conj a1 * y))
           :
           forall a2 b1 : Susp A,
           ((fun c : ... => joinl (...))
            :
            Susp A -> Join (Susp A) (Susp A)) a2 =
           ((fun d : ... => joinr (...))
            :
            Susp A -> Join (Susp A) (Susp A)) b1) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) a0 =
      ((fun b1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinr (c * b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinl (- d * conj b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            (jglue (- y * conj b1) (x * b1))^)
           :
           forall a1 b2 : Susp A,
           ((fun c : ... => joinr (...))
            :
            Susp A -> Join (Susp A) (Susp A)) a1 =
           ((fun d : ... => joinl (...))
            :
            Susp A -> Join (Susp A) (Susp A)) b2) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) b0))
  (ap idmap (jglue a b)) @ 
?Hr b = ?Hl a @ jglue a b
    1: exact (fun _ => ap joinl (hspace_right_identity _)).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall b : psusp A,
Join_rec
  ((fun a : Susp A =>
    Join_rec
      ((fun c : Susp A => joinl (a * c))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinr (conj a * d))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x y : Susp A => jglue (a * x) (conj a * y))
       :
       forall a0 b0 : Susp A,
       ((fun c : Susp A => joinl (a * c))
        :
        Susp A -> Join (Susp A) (Susp A)) a0 =
       ((fun d : Susp A => joinr (conj a * d))
        :
        Susp A -> Join (Susp A) (Susp A)) b0) pt)
   :
   Susp A -> Join (Susp A) (Susp A))
  ((fun b0 : Susp A =>
    Join_rec
      ((fun c : Susp A => joinr (c * b0))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun d : Susp A => joinl (- d * conj b0))
       :
       Susp A -> Join (Susp A) (Susp A))
      ((fun x y : Susp A =>
        (jglue (- y * conj b0) (x * b0))^)
       :
       forall a b1 : Susp A,
       ((fun c : Susp A => joinr (c * b0))
        :
        Susp A -> Join (Susp A) (Susp A)) a =
       ((fun d : Susp A => joinl (- d * conj b0))
        :
        Susp A -> Join (Susp A) (Susp A)) b1) pt)
   :
   Susp A -> Join (Susp A) (Susp A))
  ((fun a b0 : Susp A =>
    Join_ind
      (fun x : Join (Susp A) (Susp A) =>
       (fun a0 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinl (a0 * c))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinr (conj a0 * d))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x0 y : Susp A =>
            jglue (a0 * x0) (conj a0 * y))
           :
           forall a1 b1 : Susp A,
           ((fun c : Susp A => joinl (a0 * c))
            :
            Susp A -> Join (Susp A) (Susp A)) a1 =
           ((fun d : Susp A => joinr (... * d))
            :
            Susp A -> Join (Susp A) (Susp A)) b1) x) a =
       (fun b1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinr (c * b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinl (- d * conj b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x0 y : Susp A =>
            (jglue (- y * conj b1) (x0 * b1))^)
           :
           forall a0 b2 : Susp A,
           ((fun c : Susp A => joinr (c * b1))
            :
            Susp A -> Join (Susp A) (Susp A)) a0 =
           ((fun d : Susp A => joinl (... * ...))
            :
            Susp A -> Join (Susp A) (Susp A)) b2) x)
         b0)
      (fun a0 : Susp A => jglue (a * a0) (a0 * b0))
      (fun b1 : Susp A =>
       (jglue (- b1 * conj b0) (conj a * b1))^
       :
       (fun x : Join (Susp A) (Susp A) =>
        (fun a0 : Susp A =>
         Join_rec
           ((fun c : Susp A => joinl (a0 * c))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun d : Susp A => joinr (conj a0 * d))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun x0 y : Susp A =>
             jglue (a0 * x0) (conj a0 * y))
            :
            forall a1 b2 : Susp A,
            ((...) : ... -> ...) a1 =
            ((...) : ... -> ...) b2) x) a =
        (fun b2 : Susp A =>
         Join_rec
           ((fun c : Susp A => joinr (c * b2))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun d : Susp A => joinl (- d * conj b2))
            :
            Susp A -> Join (Susp A) (Susp A))
           ((fun x0 y : Susp A =>
             (jglue (... * ...) (x0 * b2))^)
            :
            forall a0 b3 : Susp A,
            ((...) : ... -> ...) a0 =
            ((...) : ... -> ...) b3) x) b0) (joinr b1))
      (fun c d : Susp A =>
       sq_dp^-1
         (sq_ccGG
            (Join_rec_beta_jglue
               (fun c0 : Susp A => joinl (a * c0))
               (fun d0 : Susp A => joinr (conj a * d0))
               (fun x y : Susp A =>
                jglue (a * x) (conj a * y)) c d)^
            (Join_rec_beta_jglue
               (fun c0 : Susp A => joinr (c0 * b0))
               (fun d0 : Susp A =>
                joinl (- d0 * conj b0))
               (fun x y : Susp A =>
                (jglue (- y * conj b0) (x * b0))^) c d)^
            (internal_paths_rew
               (fun s : Susp A =>
                PathSquare (jglue s (c * b0))
                  (jglue (- d * conj b0) (conj a * d))^
                  (jglue s (conj a * d))
                  (jglue (- d * conj b0) (c * b0))^)
               (internal_paths_rew
                  (fun s : Susp A =>
                   PathSquare
                     (jglue (f (- mon_unit)) (c * b0))
                     (jglue s (conj a * d))^
                     (jglue (f (- mon_unit))
                        (conj a * d))
                     (jglue s (c * b0))^)
                  (internal_paths_rew
                     (fun s : Susp A =>
                      PathSquare (jglue (f (...)) s)
                        (jglue (f (...)) (conj a * d))^
                        (jglue (f (...)) (conj a * d))
                        (jglue (f (...)) s)^)
                     (internal_paths_rew
                        (fun s : Susp A =>
                         PathSquare
                           (jglue (...) (...))
                           (jglue (...) s)^
                           (jglue (...) s)
                           (jglue (...) (...))^)
                        (sq_GGGG
                           (Join_rec_beta_jglue
                              (... => ...)
                              (... => ...)
                              (... => ...)
                              (- mon_unit) mon_unit)
                           (ap inverse
                              (Join_rec_beta_jglue ...
                                 ... ... ... ...))
                           (Join_rec_beta_jglue
                              (... => ...)
                              (... => ...)
                              (... => ...)
                              (- mon_unit) (... * ...))
                           (ap inverse
                              (Join_rec_beta_jglue ...
                                 ... ... ... mon_unit))
                           (sq_cGcG (ap_V ... ...)
                              (ap_V ... ...)
                              (sq_ap ... ...)))
                        (lemma4 a b0 c d))
                     (lemma3 b0 c)) (lemma2 a b0 c d))
               (lemma1 a c)))) pt)
   :
   forall a b0 : Susp A,
   ((fun a0 : Susp A =>
     Join_rec
       ((fun c : Susp A => joinl (a0 * c))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun d : Susp A => joinr (conj a0 * d))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun x y : Susp A =>
         jglue (a0 * x) (conj a0 * y))
        :
        forall a1 b1 : Susp A,
        ((fun c : Susp A => joinl (a0 * c))
         :
         Susp A -> Join (Susp A) (Susp A)) a1 =
        ((fun d : Susp A => joinr (conj a0 * d))
         :
         Susp A -> Join (Susp A) (Susp A)) b1) pt)
    :
    Susp A -> Join (Susp A) (Susp A)) a =
   ((fun b1 : Susp A =>
     Join_rec
       ((fun c : Susp A => joinr (c * b1))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun d : Susp A => joinl (- d * conj b1))
        :
        Susp A -> Join (Susp A) (Susp A))
       ((fun x y : Susp A =>
         (jglue (- y * conj b1) (x * b1))^)
        :
        forall a0 b2 : Susp A,
        ((fun c : Susp A => joinr (c * b1))
         :
         Susp A -> Join (Susp A) (Susp A)) a0 =
        ((fun d : Susp A => joinl (- d * conj b1))
         :
         Susp A -> Join (Susp A) (Susp A)) b2) pt)
    :
    Susp A -> Join (Susp A) (Susp A)) b0)
  (idmap (joinr b)) = joinr b
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap
  (Join_rec
     ((fun a0 : Susp A =>
       Join_rec
         ((fun c : Susp A => joinl (a0 * c))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinr (conj a0 * d))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           jglue (a0 * x) (conj a0 * y))
          :
          forall a1 b0 : Susp A,
          ((fun c : Susp A => joinl (a0 * c))
           :
           Susp A -> Join (Susp A) (Susp A)) a1 =
          ((fun d : Susp A => joinr (conj a0 * d))
           :
           Susp A -> Join (Susp A) (Susp A)) b0) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun b0 : Susp A =>
       Join_rec
         ((fun c : Susp A => joinr (c * b0))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinl (- d * conj b0))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           (jglue (- y * conj b0) (x * b0))^)
          :
          forall a0 b1 : Susp A,
          ((fun c : Susp A => joinr (c * b0))
           :
           Susp A -> Join (Susp A) (Susp A)) a0 =
          ((fun d : Susp A => joinl (- d * conj b0))
           :
           Susp A -> Join (Susp A) (Susp A)) b1) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun a0 b0 : Susp A =>
       Join_ind
         (fun x : Join (Susp A) (Susp A) =>
          (fun a1 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinl (a1 * c))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinr (conj a1 * d))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               jglue (a1 * x0) (conj a1 * y))
              :
              forall 
              a2 b1 : Susp A,
              ((... => ...) : Susp A -> Join ... ...)
                a2 =
              ((... => ...) : Susp A -> Join ... ...)
                b1) x) a0 =
          (fun b1 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinr (c * b1))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinl (- d * conj b1))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               (jglue (- y * conj b1) (x0 * b1))^)
              :
              forall 
              a1 b2 : Susp A,
              ((... => ...) : Susp A -> Join ... ...)
                a1 =
              ((... => ...) : Susp A -> Join ... ...)
                b2) x) b0)
         (fun a1 : Susp A => jglue (a0 * a1) (a1 * b0))
         (fun b1 : Susp A =>
          (jglue (- b1 * conj b0) (conj a0 * b1))^
          :
          (fun x : Join (Susp A) (Susp A) =>
           (fun a1 : Susp A =>
            Join_rec
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => jglue ... ...)
               :
               forall a2 b2 : Susp A, ... a2 = ... b2)
              x) a0 =
           (fun b2 : Susp A =>
            Join_rec
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => (...)^)
               :
               forall a1 b3 : Susp A, ... a1 = ... b3)
              x) b0) 
            (joinr b1))
         (fun c d : Susp A =>
          sq_dp^-1
            (sq_ccGG
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinl (a0 * c0))
                  (fun d0 : Susp A =>
                   joinr (conj a0 * d0))
                  (fun x y : Susp A =>
                   jglue (a0 * x) (conj a0 * y)) c d)^
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinr (c0 * b0))
                  (fun d0 : Susp A =>
                   joinl (- d0 * conj b0))
                  (fun x y : Susp A =>
                   (jglue (- y * conj b0) (x * b0))^)
                  c d)^
               (internal_paths_rew
                  (fun s : Susp A =>
                   PathSquare 
                    (jglue s (c * b0))
                    (jglue 
                    (- d * conj b0) 
                    (conj a0 * d))^
                    (jglue s (conj a0 * d))
                    (jglue (- d * conj b0) (c * b0))^)
                  (internal_paths_rew
                    (fun s : Susp A =>
                    PathSquare
                    (jglue (f ...) (c * b0))
                    (jglue s (... * d))^
                    (jglue (f ...) (... * d))
                    (jglue s (c * b0))^)
                    (internal_paths_rew
                    (fun s : Susp A =>
                    PathSquare 
                    (jglue ... s) 
                    (jglue ... ...)^ 
                    (jglue ... ...) 
                    (jglue ... s)^)
                    (internal_paths_rew
                    (fun ... =>
                    PathSquare ... ...^ ... ...^)
                    (sq_GGGG 
                    (...) 
                    (...) 
                    (...) 
                    (...) 
                    (...)) 
                    (lemma4 a0 b0 c d)) 
                    (lemma3 b0 c)) 
                    (lemma2 a0 b0 c d)) 
                  (lemma1 a0 c)))) pt)
      :
      forall a0 b0 : Susp A,
      ((fun a1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinl (a1 * c))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinr (conj a1 * d))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            jglue (a1 * x) (conj a1 * y))
           :
           forall a2 b1 : Susp A,
           ((fun c : ... => joinl (...))
            :
            Susp A -> Join (Susp A) (Susp A)) a2 =
           ((fun d : ... => joinr (...))
            :
            Susp A -> Join (Susp A) (Susp A)) b1) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) a0 =
      ((fun b1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinr (c * b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinl (- d * conj b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            (jglue (- y * conj b1) (x * b1))^)
           :
           forall a1 b2 : Susp A,
           ((fun c : ... => joinr (...))
            :
            Susp A -> Join (Susp A) (Susp A)) a1 =
           ((fun d : ... => joinl (...))
            :
            Susp A -> Join (Susp A) (Susp A)) b2) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) b0))
  (ap idmap (jglue a b)) @ 
?Hr b =
(fun a0 : psusp A =>
 ap joinl (hspace_right_identity a0)) a @ 
jglue a b
    1: exact (fun _ => ap joinr (hspace_left_identity _)).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap
  (Join_rec
     ((fun a0 : Susp A =>
       Join_rec
         ((fun c : Susp A => joinl (a0 * c))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinr (conj a0 * d))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           jglue (a0 * x) (conj a0 * y))
          :
          forall a1 b0 : Susp A,
          ((fun c : Susp A => joinl (a0 * c))
           :
           Susp A -> Join (Susp A) (Susp A)) a1 =
          ((fun d : Susp A => joinr (conj a0 * d))
           :
           Susp A -> Join (Susp A) (Susp A)) b0) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun b0 : Susp A =>
       Join_rec
         ((fun c : Susp A => joinr (c * b0))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinl (- d * conj b0))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           (jglue (- y * conj b0) (x * b0))^)
          :
          forall a0 b1 : Susp A,
          ((fun c : Susp A => joinr (c * b0))
           :
           Susp A -> Join (Susp A) (Susp A)) a0 =
          ((fun d : Susp A => joinl (- d * conj b0))
           :
           Susp A -> Join (Susp A) (Susp A)) b1) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun a0 b0 : Susp A =>
       Join_ind
         (fun x : Join (Susp A) (Susp A) =>
          (fun a1 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinl (a1 * c))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinr (conj a1 * d))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               jglue (a1 * x0) (conj a1 * y))
              :
              forall a2 b1 : Susp A,
              ((... => ...) : Susp A -> Join ... ...)
                a2 =
              ((... => ...) : Susp A -> Join ... ...)
                b1) x) a0 =
          (fun b1 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinr (c * b1))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinl (- d * conj b1))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               (jglue (- y * conj b1) (x0 * b1))^)
              :
              forall a1 b2 : Susp A,
              ((... => ...) : Susp A -> Join ... ...)
                a1 =
              ((... => ...) : Susp A -> Join ... ...)
                b2) x) b0)
         (fun a1 : Susp A => jglue (a0 * a1) (a1 * b0))
         (fun b1 : Susp A =>
          (jglue (- b1 * conj b0) (conj a0 * b1))^
          :
          (fun x : Join (Susp A) (Susp A) =>
           (fun a1 : Susp A =>
            Join_rec
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => jglue ... ...)
               :
               forall a2 b2 : Susp A, ... a2 = ... b2)
              x) a0 =
           (fun b2 : Susp A =>
            Join_rec
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...))
              ((fun ... => (...)^)
               :
               forall a1 b3 : Susp A, ... a1 = ... b3)
              x) b0) (joinr b1))
         (fun c d : Susp A =>
          sq_dp^-1
            (sq_ccGG
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinl (a0 * c0))
                  (fun d0 : Susp A =>
                   joinr (conj a0 * d0))
                  (fun x y : Susp A =>
                   jglue (a0 * x) (conj a0 * y)) c d)^
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinr (c0 * b0))
                  (fun d0 : Susp A =>
                   joinl (- d0 * conj b0))
                  (fun x y : Susp A =>
                   (jglue (- y * conj b0) (x * b0))^)
                  c d)^
               (internal_paths_rew
                  (fun s : Susp A =>
                   PathSquare (jglue s (c * b0))
                     (jglue (- d * conj b0)
                        (conj a0 * d))^
                     (jglue s (conj a0 * d))
                     (jglue (- d * conj b0) (c * b0))^)
                  (internal_paths_rew
                     (fun s : Susp A =>
                      PathSquare
                        (jglue (f ...) (c * b0))
                        (jglue s (... * d))^
                        (jglue (f ...) (... * d))
                        (jglue s (c * b0))^)
                     (internal_paths_rew
                        (fun s : Susp A =>
                         PathSquare (jglue ... s)
                           (jglue ... ...)^
                           (jglue ... ...)
                           (jglue ... s)^)
                        (internal_paths_rew
                           (fun ... =>
                            PathSquare ... ...^ ...
                              ...^)
                           (sq_GGGG (...) (...) (...)
                              (...) (...))
                           (lemma4 a0 b0 c d))
                        (lemma3 b0 c))
                     (lemma2 a0 b0 c d)) (lemma1 a0 c))))
         pt)
      :
      forall a0 b0 : Susp A,
      ((fun a1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinl (a1 * c))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinr (conj a1 * d))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            jglue (a1 * x) (conj a1 * y))
           :
           forall a2 b1 : Susp A,
           ((fun c : ... => joinl (...))
            :
            Susp A -> Join (Susp A) (Susp A)) a2 =
           ((fun d : ... => joinr (...))
            :
            Susp A -> Join (Susp A) (Susp A)) b1) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) a0 =
      ((fun b1 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinr (c * b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinl (- d * conj b1))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            (jglue (- y * conj b1) (x * b1))^)
           :
           forall a1 b2 : Susp A,
           ((fun c : ... => joinr (...))
            :
            Susp A -> Join (Susp A) (Susp A)) a1 =
           ((fun d : ... => joinl (...))
            :
            Susp A -> Join (Susp A) (Susp A)) b2) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) b0))
  (ap idmap (jglue a b)) @
(fun b0 : psusp A =>
 ap joinr (hspace_left_identity b0)) b =
(fun a0 : psusp A =>
 ap joinl (hspace_right_identity a0)) a @ jglue a b
    intros a b.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap
  (Join_rec
     ((fun a : Susp A =>
       Join_rec
         ((fun c : Susp A => joinl (a * c))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinr (conj a * d))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           jglue (a * x) (conj a * y))
          :
          forall a0 b : Susp A,
          ((fun c : Susp A => joinl (a * c))
           :
           Susp A -> Join (Susp A) (Susp A)) a0 =
          ((fun d : Susp A => joinr (conj a * d))
           :
           Susp A -> Join (Susp A) (Susp A)) b) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun b : Susp A =>
       Join_rec
         ((fun c : Susp A => joinr (c * b))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun d : Susp A => joinl (- d * conj b))
          :
          Susp A -> Join (Susp A) (Susp A))
         ((fun x y : Susp A =>
           (jglue (- y * conj b) (x * b))^)
          :
          forall a b0 : Susp A,
          ((fun c : Susp A => joinr (c * b))
           :
           Susp A -> Join (Susp A) (Susp A)) a =
          ((fun d : Susp A => joinl (- d * conj b))
           :
           Susp A -> Join (Susp A) (Susp A)) b0) pt)
      :
      Susp A -> Join (Susp A) (Susp A))
     ((fun a b : Susp A =>
       Join_ind
         (fun x : Join (Susp A) (Susp A) =>
          (fun a0 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinl (a0 * c))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinr (conj a0 * d))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               jglue (a0 * x0) (conj a0 * y))
              :
              forall a1 b0 : Susp A,
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...)) a1 =
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...)) b0) x) a =
          (fun b0 : Susp A =>
           Join_rec
             ((fun c : Susp A => joinr (c * b0))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun d : Susp A => joinl (- d * conj b0))
              :
              Susp A -> Join (Susp A) (Susp A))
             ((fun x0 y : Susp A =>
               (jglue (- y * conj b0) (x0 * b0))^)
              :
              forall a0 b1 : Susp A,
              ((fun ... => joinr ...)
               :
               Susp A -> Join (...) (...)) a0 =
              ((fun ... => joinl ...)
               :
               Susp A -> Join (...) (...)) b1) x) b)
         (fun a0 : Susp A => jglue (a * a0) (a0 * b))
         (fun b0 : Susp A =>
          (jglue (- b0 * conj b) (conj a * b0))^
          :
          (fun x : Join (Susp A) (Susp A) =>
           (fun a0 : Susp A =>
            Join_rec
              ((fun c : ... => joinl (...))
               :
               Susp A -> Join (Susp A) (Susp A))
              ((fun d : ... => joinr (...))
               :
               Susp A -> Join (Susp A) (Susp A))
              ((fun x0 y : ... => jglue (...) (...))
               :
               forall a1 b1 : Susp A,
               (...) a1 = (...) b1) x) a =
           (fun b1 : Susp A =>
            Join_rec
              ((fun c : ... => joinr (...))
               :
               Susp A -> Join (Susp A) (Susp A))
              ((fun d : ... => joinl (...))
               :
               Susp A -> Join (Susp A) (Susp A))
              ((fun x0 y : ... => (jglue ... ...)^)
               :
               forall a0 b2 : Susp A,
               (...) a0 = (...) b2) x) b) (joinr b0))
         (fun c d : Susp A =>
          sq_dp^-1
            (sq_ccGG
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinl (a * c0))
                  (fun d0 : Susp A =>
                   joinr (conj a * d0))
                  (fun x y : Susp A =>
                   jglue (a * x) (conj a * y)) c d)^
               (Join_rec_beta_jglue
                  (fun c0 : Susp A => joinr (c0 * b))
                  (fun d0 : Susp A =>
                   joinl (- d0 * conj b))
                  (fun x y : Susp A =>
                   (jglue (- y * conj b) (x * b))^) c
                  d)^
               (internal_paths_rew
                  (fun s : Susp A =>
                   PathSquare (jglue s (c * b))
                     (jglue (- d * conj b)
                        (conj a * d))^
                     (jglue s (conj a * d))
                     (jglue (- d * conj b) (c * b))^)
                  (internal_paths_rew
                     (fun s : Susp A =>
                      PathSquare
                        (jglue (f (...)) (c * b))
                        (jglue s (conj a * d))^
                        (jglue (f (...)) (conj a * d))
                        (jglue s (c * b))^)
                     (internal_paths_rew
                        (fun s : Susp A =>
                         PathSquare (jglue (...) s)
                           (jglue (...) (...))^
                           (jglue (...) (...))
                           (jglue (...) s)^)
                        (internal_paths_rew
                           (fun s : ... =>
                            PathSquare (...) (...)^
                              (...) (...)^)
                           (sq_GGGG
                              (Join_rec_beta_jglue ...
                                 ... ... ... mon_unit)
                              (ap inverse ...)
                              (Join_rec_beta_jglue ...
                                 ... ... ... ...)
                              (ap inverse ...)
                              (sq_cGcG ... ... ...))
                           (lemma4 a b c d))
                        (lemma3 b c)) (lemma2 a b c d))
                  (lemma1 a c)))) pt)
      :
      forall a b : Susp A,
      ((fun a0 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinl (a0 * c))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinr (conj a0 * d))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            jglue (a0 * x) (conj a0 * y))
           :
           forall a1 b0 : Susp A,
           ((fun c : Susp A => joinl (a0 * c))
            :
            Susp A -> Join (Susp A) (Susp A)) a1 =
           ((fun d : Susp A => joinr (... * d))
            :
            Susp A -> Join (Susp A) (Susp A)) b0) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) a =
      ((fun b0 : Susp A =>
        Join_rec
          ((fun c : Susp A => joinr (c * b0))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun d : Susp A => joinl (- d * conj b0))
           :
           Susp A -> Join (Susp A) (Susp A))
          ((fun x y : Susp A =>
            (jglue (- y * conj b0) (x * b0))^)
           :
           forall a0 b1 : Susp A,
           ((fun c : Susp A => joinr (c * b0))
            :
            Susp A -> Join (Susp A) (Susp A)) a0 =
           ((fun d : Susp A => joinl (... * ...))
            :
            Susp A -> Join (Susp A) (Susp A)) b1) pt)
       :
       Susp A -> Join (Susp A) (Susp A)) b))
  (ap idmap (jglue a b)) @
(fun b : psusp A => ap joinr (hspace_left_identity b))
  b =
(fun a : psusp A => ap joinl (hspace_right_identity a))
  a @ jglue a b
    refine (whiskerR _ _ @ _).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap
  (Join_rec
     (fun a : Susp A =>
      Join_rec (fun c : Susp A => joinl (a * c))
        (fun d : Susp A => joinr (conj a * d))
        (fun x y : Susp A =>
         jglue (a * x) (conj a * y)) pt)
     (fun b : Susp A =>
      Join_rec (fun c : Susp A => joinr (c * b))
        (fun d : Susp A => joinl (- d * conj b))
        (fun x y : Susp A =>
         (jglue (- y * conj b) (x * b))^) pt)
     (fun a b : Susp A =>
      Join_ind
        (fun x : Join (Susp A) (Susp A) =>
         Join_rec (fun c : Susp A => joinl (a * c))
           (fun d : Susp A => joinr (conj a * d))
           (fun x0 y : Susp A =>
            jglue (a * x0) (conj a * y)) x =
         Join_rec (fun c : Susp A => joinr (c * b))
           (fun d : Susp A => joinl (- d * conj b))
           (fun x0 y : Susp A =>
            (jglue (- y * conj b) (x0 * b))^) x)
        (fun a0 : Susp A => jglue (a * a0) (a0 * b))
        (fun b0 : Susp A =>
         (jglue (- b0 * conj b) (conj a * b0))^)
        (fun c d : Susp A =>
         sq_dp^-1
           (sq_ccGG
              (Join_rec_beta_jglue
                 (fun c0 : Susp A => joinl (a * c0))
                 (fun d0 : Susp A =>
                  joinr (conj a * d0))
                 (fun x y : Susp A =>
                  jglue (a * x) (conj a * y)) c d)^
              (Join_rec_beta_jglue
                 (fun c0 : Susp A => joinr (c0 * b))
                 (fun d0 : Susp A =>
                  joinl (- d0 * conj b))
                 (fun x y : Susp A =>
                  (jglue (- y * conj b) (x * b))^) c d)^
              (internal_paths_rew
                 (fun s : Susp A =>
                  PathSquare (jglue s (c * b))
                    (jglue (- d * conj b) (conj a * d))^
                    (jglue s (conj a * d))
                    (jglue (- d * conj b) (c * b))^)
                 (internal_paths_rew
                    (fun s : Susp A =>
                     PathSquare
                       (jglue (f (- mon_unit)) (c * b))
                       (jglue s (conj a * d))^
                       (jglue (f (- mon_unit))
                          (conj a * d))
                       (jglue s (c * b))^)
                    (internal_paths_rew
                       (fun s : Susp A =>
                        PathSquare
                          (jglue (f (- mon_unit)) s)
                          (jglue (f (... * ...))
                             (conj a * d))^
                          (jglue (f (- mon_unit))
                             (conj a * d))
                          (jglue (f (... * ...)) s)^)
                       (internal_paths_rew
                          (fun s : Susp A =>
                           PathSquare
                             (jglue (f ...)
                                (g mon_unit))
                             (jglue (f ...) s)^
                             (jglue (f ...) s)
                             (jglue (f ...)
                                (g mon_unit))^)
                          (sq_GGGG
                             (Join_rec_beta_jglue
                                (fun ... => joinl ...)
                                (fun ... => joinr ...)
                                (fun ... =>
                                 jglue ... ...)
                                (- mon_unit) mon_unit)
                             (ap inverse
                                (Join_rec_beta_jglue
                                   (...) (...) (...)
                                   (...) (...)))
                             (Join_rec_beta_jglue
                                (fun ... => joinl ...)
                                (fun ... => joinr ...)
                                (fun ... =>
                                 jglue ... ...)
                                (- mon_unit)
                                (... * d * conj b))
                             (ap inverse
                                (Join_rec_beta_jglue
                                   (...) (...) (...)
                                   (...) mon_unit))
                             (sq_cGcG
                                (ap_V (...) (...))
                                (ap_V (...) (...))
                                (sq_ap (...) (...))))
                          (lemma4 a b c d))
                       (lemma3 b c)) (lemma2 a b c d))
                 (lemma1 a c)))) pt))
  (ap idmap (jglue a b)) = ?Goal
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
?Goal @ ap joinr (hspace_left_identity b) =
ap joinl (hspace_right_identity a) @ jglue a b
    {
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap
  (Join_rec
     (fun a : Susp A =>
      Join_rec (fun c : Susp A => joinl (a * c))
        (fun d : Susp A => joinr (conj a * d))
        (fun x y : Susp A =>
         jglue (a * x) (conj a * y)) pt)
     (fun b : Susp A =>
      Join_rec (fun c : Susp A => joinr (c * b))
        (fun d : Susp A => joinl (- d * conj b))
        (fun x y : Susp A =>
         (jglue (- y * conj b) (x * b))^) pt)
     (fun a b : Susp A =>
      Join_ind
        (fun x : Join (Susp A) (Susp A) =>
         Join_rec (fun c : Susp A => joinl (a * c))
           (fun d : Susp A => joinr (conj a * d))
           (fun x0 y : Susp A =>
            jglue (a * x0) (conj a * y)) x =
         Join_rec (fun c : Susp A => joinr (c * b))
           (fun d : Susp A => joinl (- d * conj b))
           (fun x0 y : Susp A =>
            (jglue (- y * conj b) (x0 * b))^) x)
        (fun a0 : Susp A => jglue (a * a0) (a0 * b))
        (fun b0 : Susp A =>
         (jglue (- b0 * conj b) (conj a * b0))^)
        (fun c d : Susp A =>
         sq_dp^-1
           (sq_ccGG
              (Join_rec_beta_jglue
                 (fun c0 : Susp A => joinl (a * c0))
                 (fun d0 : Susp A =>
                  joinr (conj a * d0))
                 (fun x y : Susp A =>
                  jglue (a * x) (conj a * y)) c d)^
              (Join_rec_beta_jglue
                 (fun c0 : Susp A => joinr (c0 * b))
                 (fun d0 : Susp A =>
                  joinl (- d0 * conj b))
                 (fun x y : Susp A =>
                  (jglue (- y * conj b) (x * b))^) c d)^
              (internal_paths_rew
                 (fun s : Susp A =>
                  PathSquare (jglue s (c * b))
                    (jglue (- d * conj b) (conj a * d))^
                    (jglue s (conj a * d))
                    (jglue (- d * conj b) (c * b))^)
                 (internal_paths_rew
                    (fun s : Susp A =>
                     PathSquare
                       (jglue (f (- mon_unit)) (c * b))
                       (jglue s (conj a * d))^
                       (jglue (f (- mon_unit))
                          (conj a * d))
                       (jglue s (c * b))^)
                    (internal_paths_rew
                       (fun s : Susp A =>
                        PathSquare
                          (jglue (f (- mon_unit)) s)
                          (jglue (f (... * ...))
                             (conj a * d))^
                          (jglue (f (- mon_unit))
                             (conj a * d))
                          (jglue (f (... * ...)) s)^)
                       (internal_paths_rew
                          (fun s : Susp A =>
                           PathSquare
                             (jglue (f ...)
                                (g mon_unit))
                             (jglue (f ...) s)^
                             (jglue (f ...) s)
                             (jglue (f ...)
                                (g mon_unit))^)
                          (sq_GGGG
                             (Join_rec_beta_jglue
                                (fun ... => joinl ...)
                                (fun ... => joinr ...)
                                (fun ... =>
                                 jglue ... ...)
                                (- mon_unit) mon_unit)
                             (ap inverse
                                (Join_rec_beta_jglue
                                   (...) (...) (...)
                                   (...) (...)))
                             (Join_rec_beta_jglue
                                (fun ... => joinl ...)
                                (fun ... => joinr ...)
                                (fun ... =>
                                 jglue ... ...)
                                (- mon_unit)
                                (... * d * conj b))
                             (ap inverse
                                (Join_rec_beta_jglue
                                   (...) (...) (...)
                                   (...) mon_unit))
                             (sq_cGcG
                                (ap_V (...) (...))
                                (ap_V (...) (...))
                                (sq_ap (...) (...))))
                          (lemma4 a b c d))
                       (lemma3 b c)) (lemma2 a b c d))
                 (lemma1 a c)))) pt))
  (ap idmap (jglue a b)) = ?Goal refine (ap _ (ap_idmap _) @ _).
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap
  (Join_rec
     (fun a : Susp A =>
      Join_rec (fun c : Susp A => joinl (a * c))
        (fun d : Susp A => joinr (conj a * d))
        (fun x y : Susp A =>
         jglue (a * x) (conj a * y)) pt)
     (fun b : Susp A =>
      Join_rec (fun c : Susp A => joinr (c * b))
        (fun d : Susp A => joinl (- d * conj b))
        (fun x y : Susp A =>
         (jglue (- y * conj b) (x * b))^) pt)
     (fun a b : Susp A =>
      Join_ind
        (fun x : Join (Susp A) (Susp A) =>
         Join_rec (fun c : Susp A => joinl (a * c))
           (fun d : Susp A => joinr (conj a * d))
           (fun x0 y : Susp A =>
            jglue (a * x0) (conj a * y)) x =
         Join_rec (fun c : Susp A => joinr (c * b))
           (fun d : Susp A => joinl (- d * conj b))
           (fun x0 y : Susp A =>
            (jglue (- y * conj b) (x0 * b))^) x)
        (fun a0 : Susp A => jglue (a * a0) (a0 * b))
        (fun b0 : Susp A =>
         (jglue (- b0 * conj b) (conj a * b0))^)
        (fun c d : Susp A =>
         sq_dp^-1
           (sq_ccGG
              (Join_rec_beta_jglue
                 (fun c0 : Susp A => joinl (a * c0))
                 (fun d0 : Susp A =>
                  joinr (conj a * d0))
                 (fun x y : Susp A =>
                  jglue (a * x) (conj a * y)) c d)^
              (Join_rec_beta_jglue
                 (fun c0 : Susp A => joinr (c0 * b))
                 (fun d0 : Susp A =>
                  joinl (- d0 * conj b))
                 (fun x y : Susp A =>
                  (jglue (- y * conj b) (x * b))^) c d)^
              (internal_paths_rew
                 (fun s : Susp A =>
                  PathSquare (jglue s (c * b))
                    (jglue (- d * conj b) (conj a * d))^
                    (jglue s (conj a * d))
                    (jglue (- d * conj b) (c * b))^)
                 (internal_paths_rew
                    (fun s : Susp A =>
                     PathSquare
                       (jglue (f (- mon_unit)) (c * b))
                       (jglue s (conj a * d))^
                       (jglue (f (- mon_unit))
                          (conj a * d))
                       (jglue s (c * b))^)
                    (internal_paths_rew
                       (fun s : Susp A =>
                        PathSquare
                          (jglue (f (- mon_unit)) s)
                          (jglue (f (... * ...))
                             (conj a * d))^
                          (jglue (f (- mon_unit))
                             (conj a * d))
                          (jglue (f (... * ...)) s)^)
                       (internal_paths_rew
                          (fun s : Susp A =>
                           PathSquare
                             (jglue (f ...)
                                (g mon_unit))
                             (jglue (f ...) s)^
                             (jglue (f ...) s)
                             (jglue (f ...)
                                (g mon_unit))^)
                          (sq_GGGG
                             (Join_rec_beta_jglue
                                (fun ... => joinl ...)
                                (fun ... => joinr ...)
                                (fun ... =>
                                 jglue ... ...)
                                (- mon_unit) mon_unit)
                             (ap inverse
                                (Join_rec_beta_jglue
                                   (...) (...) (...)
                                   (...) (...)))
                             (Join_rec_beta_jglue
                                (fun ... => joinl ...)
                                (fun ... => joinr ...)
                                (fun ... =>
                                 jglue ... ...)
                                (- mon_unit)
                                (... * d * conj b))
                             (ap inverse
                                (Join_rec_beta_jglue
                                   (...) (...) (...)
                                   (...) mon_unit))
                             (sq_cGcG
                                (ap_V (...) (...))
                                (ap_V (...) (...))
                                (sq_ap (...) (...))))
                          (lemma4 a b c d))
                       (lemma3 b c)) (lemma2 a b c d))
                 (lemma1 a c)))) pt)) (jglue a b) =
?Goal
      simpl; rapply Join_rec_beta_jglue. }
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
jglue (a * pt) (pt * b) @
ap joinr (hspace_left_identity b) =
ap joinl (hspace_right_identity a) @ jglue a b
    symmetry.
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap joinl (hspace_right_identity a) @ jglue a b =
jglue (a * pt) (pt * b) @
ap joinr (hspace_left_identity b)
    apply join_natsq.
  Defined.

  Global Instance hspace_cdi_susp_assoc
    : IsHSpace (pjoin (psusp A) (psusp A))
    := {}.

End ImaginaroidHSpace.