CayleyDickson.v

Require Import Types.Paths.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Classes.interfaces.abstract_algebra.
Require Import Cubical.DPath Cubical.PathSquare.
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.

(** The Cayley-Dickson Construction *)

(** The Cayley-Dickson construction in homotopy type theory due to Buchholtz and Rijke https://arxiv.org/abs/1610.01134 is a method to construct an H-space structure on the join of two suspensions of a type [A]. As a special case, this gives a way to construct an H-space structure on [S^3] leading to the quarternionic Hopf fibration.

The construction works by replicating the classical Cayley-Dickson construction on convolution algebras ([*]-algebras), which can produce the complex numbers, quaternions, octonions, etc. starting with the real numbers. We cannot replicate this directly in HoTT since such algebras have a contractible underlying vector space, therefore the construction here attempts to axiomatize the properties of the units of those algebras instead.

This is done by postulating a structure called a "Cayley-Dickson imaginaroid" on a type [A] and showing that [Join (Susp A) (Susp A)] is an H-space. An open problem is to show that this space itself is also an imaginaroid given further, yet unspecified, coherences on [A]. *)

(** ** Cayley-Dickson spheroids *)

(** A Cayley-Dickson Spheroid is a pointed type X which is an H-space, with two operations called negation and conjugation, satisfying the following seven laws:
  1. [--x = x]
  2. [x** = x]
  3. [1* = 1]
  4. [(-x)* = -x*]
  5. [x(-y) = -(xy)]
  6. [(xy)* = y* x*]
  7. [x* x = 1]
Note that the above laws are written in pseudocode since we cannot define multiplication by juxtaposition in Coq, and * is used to denote conjugation. *)
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 (-) (.*.)
}.

Section CayleyDicksonSpheroid_Properties.

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

  Local Instance isequiv_cds_conjug : IsEquiv cds_conjug
    := isequiv_adjointify cds_conjug cds_conjug cds_conjug_inv cds_conjug_inv.

  #[export] 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)
    rapply (equiv_inj conj).X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj (- x * y) = conj (- (x * y))
    lhs rapply distropp.X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj y * conj (- x) = conj (- (x * y))
    rhs rapply swapop.X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj y * conj (- x) = - conj (x * y)
    rhs rapply (ap _ (distropp _ _)).X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj y * conj (- x) = - (conj y * conj x)
    rhs_V rapply factorneg_r.X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj y * conj (- x) = conj y * - conj x
    napply ap.X: pType
H: CayleyDicksonSpheroid X
x, y: X
conj (- x) = - conj x
    apply swapop.
  Defined.

  #[export] Instance cds_conjug_right_inv : RightInverse (.*.) cds_conjug mon_unit.X: pType
H: CayleyDicksonSpheroid X
RightInverse sg_op cds_conjug 1
  Proof.X: pType
H: CayleyDicksonSpheroid X
RightInverse sg_op cds_conjug 1
    intro x.X: pType
H: CayleyDicksonSpheroid X
x: X
x * cds_conjug x = 1
    lhs_V exact (ap (.* conj x) (involutive x)).X: pType
H: CayleyDicksonSpheroid X
x: X
cds_conjug (cds_conjug x) * conj x = 1
    rapply left_inverse.
  Defined.

End CayleyDicksonSpheroid_Properties.

(** ** Negation and conjugation on suspensions *)

Instance conjugate_susp (A : Type) `(Negate A) : Conjugate (Susp A)
  := functor_susp (-).

Instance negate_susp (A : Type) `(Negate A) : Negate (Susp A)
  := susp_neg _ o conjugate_susp A (-).

(** [conjugate_susp A] and [negate_susp A] commute. *)
Instance swapop_conjugate_susp {A} `(Negate A)
  : SwapOp (negate_susp A (-)) (conjugate_susp A (-)).A: Type
H: Negate A
SwapOp (negate_susp A negate)
  (conjugate_susp A negate)
Proof.A: Type
H: Negate A
SwapOp (negate_susp A negate)
  (conjugate_susp A negate)
  intros x.A: Type
H: Negate A
x: Susp A
conj (- x) = - conj x
  symmetry.A: Type
H: Negate A
x: Susp A
- conj x = conj (- x)
  napply susp_neg_natural.
Defined.

(** [conjugate_susp A] is involutive, since any functor applied to an involution gives an involution. *)
Instance involutive_conjugate_susp {A} `(Negate A, !Involutive (-))
  : Involutive (conjugate_susp A (-)).A: Type
H: Negate A
Involutive0: Involutive negate
Involutive (conjugate_susp A negate)
Proof.A: Type
H: Negate A
Involutive0: Involutive negate
Involutive (conjugate_susp A negate)
  intros x.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
conjugate_susp A negate (conjugate_susp A negate x) =
x
  lhs_V napply functor_susp_compose.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
functor_susp (fun x : A => - - x) x = x
  rhs_V napply functor_susp_idmap.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
functor_susp (fun x : A => - - x) x =
functor_susp idmap x
  napply functor2_susp.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
(fun x : A => - - x) == idmap
  exact involutive.
Defined.

(** [conjugate_susp A] is involutive as any composite of commuting involutions is an involution. *)
Instance involutive_negate_susp {A} `(Negate A, !Involutive (-))
  : Involutive (negate_susp A (-)).A: Type
H: Negate A
Involutive0: Involutive negate
Involutive (negate_susp A negate)
Proof.A: Type
H: Negate A
Involutive0: Involutive negate
Involutive (negate_susp A negate)
  intros x.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
negate_susp A negate (negate_susp A negate x) = x
  unfold negate_susp.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
susp_neg A
  (conjugate_susp A negate
     (susp_neg A (conjugate_susp A negate x))) = x
  lhs napply ap.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
conjugate_susp A negate
  (susp_neg A (conjugate_susp A negate x)) = ?Goal
A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
susp_neg A ?Goal = x
  1: napply swapop_conjugate_susp.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
susp_neg A (- conj x) = x
  lhs rapply susp_neg_inv.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
conjugate_susp A negate (conj x) = x
  rapply involutive.
Defined.

(** ** Cayley-Dickson imaginaroids *)

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);
}.

Instance isunitpreserving_conjugate_susp {A} `(CayleyDicksonImaginaroid A)
  : @IsUnitPreserving _ _ pt pt (conjugate_susp A cdi_negate)
  := idpath.

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

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) 1
Proof.A: Type
H: CayleyDicksonImaginaroid A
LeftInverse hspace_op (conjugate_susp A cdi_negate) 1
  exact cds_conjug_left_inv.
Defined.

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) 1
Proof.A: Type
H: CayleyDicksonImaginaroid A
RightInverse hspace_op (conjugate_susp A cdi_negate) 1
  stapply cds_conjug_right_inv.
Defined.

Instance cdi_susp_left_identity {A} `(CayleyDicksonImaginaroid A)
  : LeftIdentity hspace_op mon_unit
  := _.

Instance cdi_susp_right_identity {A} `(CayleyDicksonImaginaroid A)
  : RightIdentity hspace_op mon_unit
  := _.

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
  stapply cds_factorneg_l.
Defined.

(** A Cayley-Dickson imaginaroid [A] whose multiplication on the suspension is associative gives rise to an 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 (- (1)) = a * c
    Proof.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
f (- (1)) = a * c
      unfold f; apply ap.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * - - (1) = 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
- (1 * 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 1 = c * b
    Proof.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
g 1 = c * b
      unfold g; apply ap.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
1 * 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) * 1 = 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
1 * conj a * d = conj a * d
      rewrite <- simple_associativity.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
1 * (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. *)
  #[export] 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))
    snapply Join_rec2.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a c d : psusp A, ?P_AC a c = ?P_AD a d
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall b c d : psusp A, ?P_BC b c = ?P_BD b d
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall c a b : psusp A, ?P_AC a c = ?P_BC b c
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall d a b : psusp A, ?P_AD a d = ?P_BD b d
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b c d : psusp A,
?P_gAx a c d @ ?P_gxD d a b =
?P_gxC c a b @ ?P_gBx b c d
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A) exact (fun a b => joinl (a * b)).
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A) exact (fun a b => joinr (conj a * b)).
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A) exact (fun a b => joinr (b * a)).
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
psusp A -> psusp A -> pjoin (psusp A) (psusp A) exact (fun a b => joinl ((- b) * conj a)).
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a c d : psusp A,
(fun a0 b : psusp A => joinl (a0 * b)) a c =
(fun a0 b : psusp A => joinr (conj a0 * b)) a d intros; apply jglue.
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall b c d : psusp A,
(fun a b0 : psusp A => joinr (b0 * a)) b c =
(fun a b0 : psusp A => joinl (- b0 * conj a)) b d intros; symmetry; apply jglue.
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall c a b : psusp A,
(fun a0 b0 : psusp A => joinl (a0 * b0)) a c =
(fun a0 b0 : psusp A => joinr (b0 * a0)) b c intros; apply jglue.
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall d a b : psusp A,
(fun a0 b0 : psusp A => joinr (conj a0 * b0)) a d =
(fun a0 b0 : psusp A => joinl (- b0 * conj a0)) b d intros; symmetry; apply jglue.
    -A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b c d : psusp A,
(fun a0 c0 d0 : psusp A =>
 jglue (a0 * c0) (conj a0 * d0)) a c d @
(fun d0 a0 b0 : psusp A =>
 (jglue (- d0 * conj b0) (conj a0 * d0))^) d a b =
(fun c0 a0 b0 : psusp A => jglue (a0 * c0) (c0 * b0))
  c a b @
(fun b0 c0 d0 : psusp A =>
 (jglue (- d0 * conj b0) (c0 * b0))^) b c d intros a b c d; cbn beta.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
jglue (a * c) (conj a * d) @
(jglue (- d * conj b) (conj a * d))^ =
jglue (a * c) (c * b) @
(jglue (- d * conj b) (c * b))^
      symmetry.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
jglue (a * c) (c * b) @
(jglue (- d * conj b) (c * b))^ =
jglue (a * c) (conj a * d) @
(jglue (- d * conj b) (conj a * d))^
      apply sq_path.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp 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).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
PathSquare (jglue (f (- (1))) (c * b))
  (jglue (- d * conj b) (conj a * d))^
  (jglue (f (- (1))) (conj a * d))
  (jglue (- d * conj b) (c * b))^
      rewrite <- (lemma2 a b c d).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
PathSquare (jglue (f (- (1))) (c * b))
  (jglue (f (conj c * conj a * d * conj b))
     (conj a * d))^ (jglue (f (- (1))) (conj a * d))
  (jglue (f (conj c * conj a * d * conj b)) (c * b))^
      rewrite <- (lemma3 b c).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
PathSquare (jglue (f (- (1))) (g 1))
  (jglue (f (conj c * conj a * d * conj b))
     (conj a * d))^ (jglue (f (- (1))) (conj a * d))
  (jglue (f (conj c * conj a * d * conj b))
     (g mon_unit))^
      rewrite <- (lemma4 a b c d).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
PathSquare (jglue (f (- (1))) (g 1))
  (jglue (f (conj c * conj a * d * conj b))
     (g (conj c * conj a * d * conj b)))^
  (jglue (f (- (1)))
     (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: psusp A
?Goal = jglue (f (- (1))) (g 1)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
?Goal0 =
(jglue (f (conj c * conj a * d * conj b))
   (g (conj c * conj a * d * conj b)))^%path
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
?Goal1 =
jglue (f (- (1))) (g (conj c * conj a * d * conj b))
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
?Goal2 =
(jglue (f (conj c * conj a * d * conj b)) (g mon_unit))^%path
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
PathSquare ?Goal ?Goal0 ?Goal1 ?Goal2
      2,4: apply ap.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
?Goal = jglue (f (- (1))) (g 1)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp 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: psusp A
?x0 = jglue (f (conj c * conj a * d * conj b)) (g 1)
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
?Goal0 =
jglue (f (- (1))) (g (conj c * conj a * d * conj b))
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp 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: psusp 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 (- (1)) 1))
  (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 (- (1)) (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: psusp 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)))^%path
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp 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))^%path
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp 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 (- (1)) 1)) 
  ?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 (- (1)) (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: psusp 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 (- (1)) 1))
  (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 (- (1)) (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: psusp A
PathSquare (jglue (- (1)) 1)
  (jglue (conj c * conj a * d * conj b)
     (conj c * conj a * d * conj b))^
  (jglue (- (1)) (conj c * conj a * d * conj b))
  (jglue (conj c * conj a * d * conj b) mon_unit)^
      change (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)^).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
PathSquare (jglue (- (1)) 1)
  (jglue (conj c * conj a * d * conj b)
     (conj c * conj a * d * conj b))^
  (jglue (- (1)) (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: psusp A
forall p : psusp A,
PathSquare (jglue (- (1)) 1) (jglue p p)^
  (jglue (- (1)) p) (jglue p mon_unit)^
      clear a b c d.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall p : psusp A,
PathSquare (jglue (- (1)) 1) (jglue p p)^
  (jglue (- (1)) p) (jglue p 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 (- (1)) s 1 s
      srapply Susp_ind; hnf.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
PathSquare (jglue (- (1)) 1) (jglue North North)^
  (jglue (- (1)) North) (jglue North mon_unit)^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
PathSquare (jglue (- (1)) 1) 
  (jglue South South)^ 
  (jglue (- (1)) South) 
  (jglue South mon_unit)^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall x : A,
transport (fun y : Susp A => Diamond (- (1)) y 1 y)
  (merid x) ?Goal = ?Goal0
      1: by apply diamond_v_sq.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
PathSquare (jglue (- (1)) 1) (jglue South South)^
  (jglue (- (1)) South) (jglue South mon_unit)^
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall x : A,
transport (fun y : Susp A => Diamond (- (1)) y 1 y)
  (merid x) (diamond_v_sq (- (1)) 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 (- (1)) y 1 y)
  (merid x) (diamond_v_sq (- (1)) North 1) =
diamond_h_sq 1 South 1
      intro a.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a: A
transport (fun y : Susp A => Diamond (- (1)) y 1 y)
  (merid a) (diamond_v_sq (- (1)) North 1) =
diamond_h_sq 1 South 1
      apply diamond_twist.
  Defined.

  #[export] 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
    snapply Join_ind_Flr.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a : psusp A, cd_op pt (joinl a) = joinl a
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall b : psusp A, cd_op pt (joinr b) = joinr b
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap (cd_op pt) (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) (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) (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 napply whiskerR.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap (cd_op pt) (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
    1: exact (Join_rec_beta_jglue _ _ _ 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.

  #[export] 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
    snapply Join_ind_Flr.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a : psusp A,
(fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (joinl a) = joinl a
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall b : psusp A,
(fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (joinr b) = joinr b
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap (fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (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,
(fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (joinr b) = joinr b
A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
forall a b : psusp A,
ap (fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (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 (fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (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 (fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (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
    lhs napply whiskerR.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
ap (fun x : Join (psusp A) (psusp A) => cd_op x pt)
  (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
    1: exact (Join_rec_beta_jglue _ _ _ a b).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b: psusp A
Join_ind_FlFr
  (fun x : Join (psusp A) (psusp A) =>
   (fun a : psusp A =>
    Join_rec
      ((fun a0 b : psusp A => joinl (a0 * b)) a)
      ((fun a0 b : psusp A => joinr (conj a0 * b)) a)
      ((fun a0 c d : psusp A =>
        jglue (a0 * c) (conj a0 * d)) a) x) a)
  (fun x : Join (psusp A) (psusp A) =>
   (fun b : psusp A =>
    Join_rec
      ((fun a b0 : psusp A => joinr (b0 * a)) b)
      ((fun a b0 : psusp A => joinl (- b0 * conj a)) b)
      ((fun b0 c d : psusp A =>
        (jglue (- d * conj b0) (c * b0))^) b) x) b)
  (fun c : psusp A =>
   (fun c0 a b : psusp A => jglue (a * c0) (c0 * b)) c
     a b)
  (fun d : psusp A =>
   (fun d0 a b : psusp A =>
    (jglue (- d0 * conj b) (conj a * d0))^) d a b)
  (fun c d : psusp A =>
   whiskerR
     (Join_rec_beta_jglue
        ((fun a b : psusp A => joinl (a * b)) a)
        ((fun a b : psusp A => joinr (conj a * b)) a)
        ((fun a c0 d0 : psusp A =>
          jglue (a * c0) (conj a * d0)) a) c d)
     ((fun d0 a b : psusp A =>
       (jglue (- d0 * conj b) (conj a * d0))^) d a b) @
   ((fun a b c0 d0 : psusp A =>
     (let X := equiv_isequiv sq_path in
      let X0 := sq_path^-1 in
      X0
        (internal_paths_rew
           (fun s : Susp A =>
            PathSquare (jglue s (c0 * b))
              (jglue (- d0 * conj b) (conj a * d0))^
              (jglue s (conj a * d0))
              (jglue (- d0 * conj b) (c0 * b))^)
           (internal_paths_rew
              (fun s : Susp A =>
               PathSquare (jglue (...) (...))
                 (jglue s (...))^ (jglue (...) (...))
                 (jglue s (...))^)
              (internal_paths_rew
                 (fun s : ... =>
                  PathSquare (...) (...)^ (...) (...)^)
                 (internal_paths_rew (... => ...)
                    (sq_GGGG ... ... ... ... ...)
                    (lemma4 a b c0 d0)) (lemma3 b c0))
              (lemma2 a b c0 d0)) (lemma1 a c0)))^
     :
     (fun a0 c1 d1 : psusp A =>
      jglue (a0 * c1) (conj a0 * d1)) a c0 d0 @
     (fun d1 a0 b0 : psusp A =>
      (jglue (- d1 * conj b0) (conj a0 * d1))^) d0 a b =
     (fun c1 a0 b0 : psusp A =>
      jglue (a0 * c1) (c1 * b0)) c0 a b @
     (fun b0 c1 d1 : psusp A =>
      (jglue (- d1 * conj b0) (c1 * b0))^) b c0 d0) a
      b c d @
    (whiskerL
       ((fun c0 a b : psusp A =>
         jglue (a * c0) (c0 * b)) c a b)
       (Join_rec_beta_jglue
          ((fun a b : psusp A => joinr (b * a)) b)
          ((fun a b : psusp A => joinl (- b * conj a))
             b)
          ((fun b c0 d0 : psusp A =>
            (jglue (- d0 * conj b) (c0 * b))^) b) c d))^)
   :
   ap
     (fun x : Join (psusp A) (psusp A) =>
      (fun a : psusp A =>
       Join_rec
         ((fun a0 b : psusp A => joinl (a0 * b)) a)
         ((fun a0 b : psusp A => joinr (conj a0 * b))
            a)
         ((fun a0 c0 d0 : psusp A =>
           jglue (a0 * c0) (conj a0 * d0)) a) x) a)
     (jglue c d) @
   (fun d0 : psusp A =>
    (fun d1 a b : psusp A =>
     (jglue (- d1 * conj b) (conj a * d1))^) d0 a b) d =
   (fun c0 : psusp A =>
    (fun c1 a b : psusp A => jglue (a * c1) (c1 * b))
      c0 a b) c @
   ap
     (fun x : Join (psusp A) (psusp A) =>
      (fun b : psusp A =>
       Join_rec
         ((fun a b0 : psusp A => joinr (b0 * a)) b)
         ((fun a b0 : psusp A => joinl (- b0 * conj a))
            b)
         ((fun b0 c0 d0 : psusp A =>
           (jglue (- d0 * conj b0) (c0 * b0))^) b) x)
        b) (jglue c d)) pt @
ap joinr (hspace_left_identity b) =
ap joinl (hspace_right_identity a) @ jglue a b
    simpl; 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.

  #[export] Instance hspace_cdi_susp_assoc
    : IsHSpace (pjoin (psusp A) (psusp A))
    := {}.

End ImaginaroidHSpace.