HoTT.Homotopy.CayleyDickson.v.alectryon.json

From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Classes.interfaces.abstract_algebra Classes.theory.groups.
Require Import Pointed.Core Pointed.pSusp.
Require Import Homotopy.HSpace.Core.
Require Import Homotopy.Suspension.
Require Import Homotopy.Join.Core Homotopy.Join.JoinSusp.

Local Open Scope pointed_scope.
Local Open Scope mc_mult_scope.
Local Open Scope path_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 quaternionic 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_involution cds_conjug 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 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
    lhs_V exact (ap (.* conj x) (involutive x)).X: pType
H: CayleyDicksonSpheroid X
x: X
cds_conjug (cds_conjug x) * conj x = mon_unit
    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 x0 : A => - - x0) x = x
  rhs_V napply functor_susp_idmap.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
functor_susp (fun x0 : A => - - x0) x = functor_susp idmap x
  napply functor2_susp.A: Type
H: Negate A
Involutive0: Involutive negate
x: Susp A
(fun x0 : A => - - x0) == idmap
  exact involutive.
Defined.

(** [negate_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} `(Negate A)
  : @IsUnitPreserving _ _ pt pt (conjugate_susp A _)
  := 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_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
  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.

  Local Definition cd_diamond_map_l (a c : Susp A)
    := fun x => a * (c * -x).
  Local Definition cd_diamond_map_r (b c : Susp A)
    := fun y => c * (y * b).

  Section ScalarBoundary.

    Context (a b c d : Susp A).

    Lemma cd_diamond_map_l_neg_unit
      : cd_diamond_map_l a c (- mon_unit) = a * c.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
cd_diamond_map_l a c (- mon_unit) = a * c
    Proof.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
cd_diamond_map_l a c (- mon_unit) = a * c
      unfold cd_diamond_map_l; 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 cd_diamond_map_l_parameter
      : cd_diamond_map_l a c ((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
cd_diamond_map_l a c (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
cd_diamond_map_l a c (conj c * (conj a * d) * conj b) = - d * conj b
      unfold cd_diamond_map_l.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
      lhs tapply (ap (a *.) (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
      lhs tapply 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
      rhs tapply factorneg_l.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)
      napply ap.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
      lhs tapply (ap (a *.) (simple_associativity (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
      lhs tapply (simple_associativity (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
      napply (ap (.* conj b)).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
a * (c * (conj c * (conj a * d))) = d
      lhs tapply (ap (a *.) (sgop_inv_g_Vg c _)).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
a * (conj a * d) = d
      rapply sgop_inv_g_Vg.
    Defined.

    Lemma cd_diamond_map_r_unit
      : cd_diamond_map_r b c mon_unit = c * b.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
cd_diamond_map_r b c mon_unit = c * b
    Proof.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
cd_diamond_map_r b c mon_unit = c * b
      unfold cd_diamond_map_r; 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 cd_diamond_map_r_parameter
      : cd_diamond_map_r b c ((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
cd_diamond_map_r b c (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
cd_diamond_map_r b c (conj c * (conj a * d) * conj b) = conj a * d
      unfold cd_diamond_map_r.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
      lhs tapply (ap (c *.) (sgop_inv_gV_g _ b)).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: Susp A
c * (conj c * (conj a * d)) = conj a * d
      tapply sgop_inv_g_Vg.
    Defined.

  End ScalarBoundary.

  (** 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))^
      change (diamond (a * c) ((-d) * conj b) (c * b) (conj a * d)).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
diamond (a * c) (- d * conj b) (c * b) (conj a * d)
      rewrite <- (cd_diamond_map_l_neg_unit a c).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
diamond (cd_diamond_map_l a c (- mon_unit)) (- d * conj b) 
  (c * b) (conj a * d)
      (** Rewrite this corner first since the other also contains [conj a * d]. *)
      rewrite <- (cd_diamond_map_r_parameter a b c d).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
diamond (cd_diamond_map_l a c (- mon_unit)) (- d * conj b) 
  (c * b) (cd_diamond_map_r b c (conj c * (conj a * d) * conj b))
      rewrite <- (cd_diamond_map_l_parameter a b c d).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
diamond (cd_diamond_map_l a c (- mon_unit))
  (cd_diamond_map_l a c (conj c * (conj a * d) * conj b)) 
  (c * b) (cd_diamond_map_r b c (conj c * (conj a * d) * conj b))
      rewrite <- (cd_diamond_map_r_unit b c).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
diamond (cd_diamond_map_l a c (- mon_unit))
  (cd_diamond_map_l a c (conj c * (conj a * d) * conj b))
  (cd_diamond_map_r b c mon_unit)
  (cd_diamond_map_r b c (conj c * (conj a * d) * conj b))
      napply (functor_diamond (cd_diamond_map_l a c) (cd_diamond_map_r b c)).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
a, b, c, d: psusp A
diamond (- mon_unit) (conj c * (conj a * d) * conj b) mon_unit
  (conj c * (conj a * d) * conj b)
      apply diamond_susp.
  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
    intro z; simpl.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
z: pjoin (psusp A) (psusp A)
Join_rec (fun b : Susp A => joinl (pt * b))
  (fun b : Susp A => joinr (conj pt * b))
  (fun c d : Susp A => jglue (pt * c) (conj pt * d)) z =
z
    lhs exact (functor2_join hspace_left_identity hspace_left_identity z).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
z: pjoin (psusp A) (psusp A)
functor_join idmap idmap z = z
    napply functor_join_idmap.
  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
    intro z.A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
z: pjoin (psusp A) (psusp A)
cd_op z pt = z
    (* This one doesn't simplify to a nice term, but a similar proof works. *)
    lhs napply (functor2_join hspace_right_identity hspace_left_identity).A: Type
H: CayleyDicksonImaginaroid A
Associative0: Associative hspace_op
z: pjoin (psusp A) (psusp A)
functor_join idmap idmap z = z
    napply functor_join_idmap.
  Defined.

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

End ImaginaroidHSpace.