Require Import Basics Types HSpace.Core HSpace.Coherent HSpace.Pointwise
  Pointed Homotopy.EvaluationFibration.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope pointed_scope.
Local Open Scope mc_mult_scope.
Local Open Scope path_scope.

(** * The moduli type of coherent H-space structures *)

(** When [A] is a left-invertible coherent H-space, we construct an equivalence between the ("moduli") type of coherent H-space structures on [A] and the type [A ->* (A ->** A)]. By the smash-hom adjunction for pointed types, due to Floris van Doorn in HoTT, the latter is also equivalent to the type [Smash A A ->* A].

This equivalence generalizes a formula of Arkowitz--Curjel and Copeland for spaces, and appears as Theorem 2.27 in https://arxiv.org/abs/2301.02636v1 *)

(** ** Paths between H-space structures *)

(** Paths between H-space structures correspond to homotopies between the underlying binary operations which respect the identities. This is the type of the latter. *)
Definition path_ishspace_type {X : pType} (mu nu : IsHSpace X) : Type.
X: pType
mu, nu: IsHSpace X
Type
Proof.
X: pType
mu, nu: IsHSpace X
Type
  destruct mu as [mu mu_lid mu_rid], nu as [nu nu_lid nu_rid].
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
Type
  refine { h : forall x0 x1, mu x0 x1 = nu x0 x1 & prod (forall x:X, _) (forall x:X, _) }.
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x0 x1 : X, mu x0 x1 = nu x0 x1
x: X
Type
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x0 x1 : X, mu x0 x1 = nu x0 x1
x: X
Type
  -
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x0 x1 : X, mu x0 x1 = nu x0 x1
x: X
Type exact (mu_lid x = h pt x @ nu_lid x).
  -
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x0 x1 : X, mu x0 x1 = nu x0 x1
x: X
Type exact (mu_rid x = h x pt @ nu_rid x).
Defined.

(** Transport of left and right identities of binary operations along paths between the underlying functions. *)
Local Definition transport_binop_lr_id `{Funext} {X : Type} {x : X}
  {mu nu : X -> X -> X} `{mu_lid : forall y, mu x y = y}
  `{mu_rid : forall y, mu y x = y} (p : mu = nu)
  : transport (fun m : X -> X -> X =>
                 (forall y, m x y = y) * (forall y, m y x = y))
      p (mu_lid, mu_rid)
    = (fun y => (ap100 p _ _)^ @ mu_lid y,
         fun y => (ap100 p _ _)^ @ mu_rid y).
H: Funext
X: Type
x: X
mu, nu: X -> X -> X
mu_lid: forall y : X, mu x y = y
mu_rid: forall y : X, mu y x = y
p: mu = nu
transport
  (fun m : X -> X -> X =>
   (forall y : X, m x y = y) *
   (forall y : X, m y x = y)) p (mu_lid, mu_rid) =
(fun y : X => (ap100 p x y)^ @ mu_lid y,
fun y : X => (ap100 p y x)^ @ mu_rid y)
Proof.
H: Funext
X: Type
x: X
mu, nu: X -> X -> X
mu_lid: forall y : X, mu x y = y
mu_rid: forall y : X, mu y x = y
p: mu = nu
transport
  (fun m : X -> X -> X =>
   (forall y : X, m x y = y) *
   (forall y : X, m y x = y)) p 
  (mu_lid, mu_rid) =
(fun y : X => (ap100 p x y)^ @ mu_lid y,
fun y : X => (ap100 p y x)^ @ mu_rid y)
  induction p; cbn.
H: Funext
X: Type
x: X
mu: X -> X -> X
mu_lid: forall y : X, mu x y = y
mu_rid: forall y : X, mu y x = y
(mu_lid, mu_rid) =
(fun y : X => 1 @ mu_lid y, fun y : X => 1 @ mu_rid y)
  apply path_prod'; funext y.
H: Funext
X: Type
x: X
mu: X -> X -> X
mu_lid: forall y : X, mu x y = y
mu_rid: forall y : X, mu y x = y
y: X
mu_lid y = 1 @ mu_lid y
H: Funext
X: Type
x: X
mu: X -> X -> X
mu_lid: forall y : X, mu x y = y
mu_rid: forall y : X, mu y x = y
y: X
mu_rid y = 1 @ mu_rid y
  all: exact (concat_1p _)^.
Defined.

(** Characterization of paths between H-space structures. *)
Definition equiv_path_ishspace `{Funext} {X : pType} (mu nu : IsHSpace X)
  : path_ishspace_type mu nu <~> (mu = nu).
H: Funext
X: pType
mu, nu: IsHSpace X
path_ishspace_type mu nu <~> mu = nu
Proof.
H: Funext
X: pType
mu, nu: IsHSpace X
path_ishspace_type mu nu <~> mu = nu
  destruct mu as [mu mu_lid mu_rid], nu as [nu nu_lid nu_rid];
    unfold path_ishspace_type.
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
{h : forall x0 x1 : X, mu x0 x1 = nu x0 x1 &
((forall x : X, mu_lid x = h pt x @ nu_lid x) *
 (forall x : X, mu_rid x = h x pt @ nu_rid x))%type} <~>
{|
  hspace_op := mu;
  hspace_left_identity := mu_lid;
  hspace_right_identity := mu_rid
|} =
{|
  hspace_op := nu;
  hspace_left_identity := nu_lid;
  hspace_right_identity := nu_rid
|}
  nrefine (equiv_ap_inv' issig_ishspace _ _ oE _).
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
{h : forall x0 x1 : X, mu x0 x1 = nu x0 x1 &
((forall x : X, mu_lid x = h pt x @ nu_lid x) *
 (forall x : X, mu_rid x = h x pt @ nu_rid x))%type} <~>
issig_ishspace^-1
  {|
    hspace_op := mu;
    hspace_left_identity := mu_lid;
    hspace_right_identity := mu_rid
  |} =
issig_ishspace^-1
  {|
    hspace_op := nu;
    hspace_left_identity := nu_lid;
    hspace_right_identity := nu_rid
  |}
  nrefine (equiv_path_sigma _ _ _ oE _); cbn.
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
{h : forall x0 x1 : X, mu x0 x1 = nu x0 x1 &
((forall x : X, mu_lid x = h pt x @ nu_lid x) *
 (forall x : X, mu_rid x = h x pt @ nu_rid x))%type} <~>
{p : mu = nu &
transport
  (fun mu : X -> X -> X =>
   ((forall x : X, mu pt x = x) *
    (forall x : X, mu x pt = x))%type) p
  (mu_lid, mu_rid) = (nu_lid, nu_rid)}
  apply (equiv_functor_sigma' (equiv_path_arrow2 _ _)); intro h; cbn.
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x y : X, mu x y = nu x y
(forall x : X, mu_lid x = h pt x @ nu_lid x) *
(forall x : X, mu_rid x = h x pt @ nu_rid x) <~>
transport
  (fun mu : X -> X -> X =>
   ((forall x : X, mu pt x = x) *
    (forall x : X, mu x pt = x))%type)
  (path_forall mu nu
     (functor_forall idmap
        (fun a : X => path_forall (mu a) (nu a)) h))
  (mu_lid, mu_rid) = (nu_lid, nu_rid)
  nrefine (equiv_concat_l _ _ oE _).
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x y : X, mu x y = nu x y
transport
  (fun mu : X -> X -> X =>
   ((forall x : X, mu pt x = x) *
    (forall x : X, mu x pt = x))%type)
  (path_forall mu nu
     (functor_forall idmap
        (fun a : X => path_forall (mu a) (nu a)) h))
  (mu_lid, mu_rid) = ?Goal
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x y : X, mu x y = nu x y
(forall x : X, mu_lid x = h pt x @ nu_lid x) *
(forall x : X, mu_rid x = h x pt @ nu_rid x) <~>
?Goal = (nu_lid, nu_rid)
  1: apply transport_binop_lr_id.
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x y : X, mu x y = nu x y
(forall x : X, mu_lid x = h pt x @ nu_lid x) *
(forall x : X, mu_rid x = h x pt @ nu_rid x) <~>
(fun y : X =>
 (ap100
    (path_forall mu nu
       (functor_forall idmap
          (fun a : X => path_forall (mu a) (nu a)) h))
    pt y)^ @ mu_lid y,
fun y : X =>
(ap100
   (path_forall mu nu
      (functor_forall idmap
         (fun a : X => path_forall (mu a) (nu a)) h))
   y pt)^ @ mu_rid y) = 
(nu_lid, nu_rid)
  nrefine (equiv_path_prod _ _ oE _); cbn.
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x y : X, mu x y = nu x y
(forall x : X, mu_lid x = h pt x @ nu_lid x) *
(forall x : X, mu_rid x = h x pt @ nu_rid x) <~>
((fun y : X =>
  (ap100
     (path_forall mu nu
        (functor_forall idmap
           (fun a : X => path_forall (mu a) (nu a)) h))
     pt y)^ @ mu_lid y) = nu_lid) *
((fun y : X =>
  (ap100
     (path_forall mu nu
        (functor_forall idmap
           (fun a : X => path_forall (mu a) (nu a)) h))
     y pt)^ @ mu_rid y) = nu_rid)
  apply equiv_functor_prod';
    nrefine (equiv_path_forall _ _ oE _);
    apply equiv_functor_forall_id; intro x.
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x y : X, mu x y = nu x y
x: X
mu_lid x = h pt x @ nu_lid x <~>
(ap100
   (path_forall mu nu
      (functor_forall idmap
         (fun a : X => path_forall (mu a) (nu a)) h))
   pt x)^ @ mu_lid x = nu_lid x
H: Funext
X: pType
mu: SgOp X
mu_lid: LeftIdentity mu pt
mu_rid: RightIdentity mu pt
nu: SgOp X
nu_lid: LeftIdentity nu pt
nu_rid: RightIdentity nu pt
h: forall x y : X, mu x y = nu x y
x: X
mu_rid x = h x pt @ nu_rid x <~>
(ap100
   (path_forall mu nu
      (functor_forall idmap
         (fun a : X => path_forall (mu a) (nu a)) h))
   x pt)^ @ mu_rid x = nu_rid x
  all: nrefine (equiv_moveR_Vp _ _ _ oE _);
    apply equiv_concat_r;
    apply whiskerR; symmetry;
    apply ap100_path_arrow2.
Defined.

(** ** Sections of evaluation fibrations *)

(** We first show that coherent H-space structures on a pointed type correspond to pointed sections of the evaluation fibration [ev A]. *)
Definition equiv_iscohhspace_psect `{Funext} (A : pType)
  : IsCohHSpace A <~> pSect (ev A).
H: Funext
A: pType
IsCohHSpace A <~> pSect (ev A)
Proof.
H: Funext
A: pType
IsCohHSpace A <~> pSect (ev A)
  refine (issig_psect (ev A) oE _^-1%equiv oE (issig_iscohhspace A)^-1%equiv).
H: Funext
A: pType
{s : A -> selfmaps A &
{p : s pt = pt &
{H : (fun x : A => ev A (s x)) == idmap &
H pt = ap (ev A) p @ point_eq (ev A)}}} <~>
{hspace_op : SgOp A &
{hspace_left_identity : LeftIdentity hspace_op pt &
{hspace_right_identity : RightIdentity hspace_op pt &
hspace_left_identity pt = hspace_right_identity pt}}}
  unfold SgOp, LeftIdentity, RightIdentity.
H: Funext
A: pType
{s : A -> selfmaps A &
{p : s pt = pt &
{H : (fun x : A => ev A (s x)) == idmap &
H pt = ap (ev A) p @ point_eq (ev A)}}} <~>
{hspace_op : A -> A -> A &
{hspace_left_identity
: forall y : A, hspace_op pt y = y &
{hspace_right_identity
: forall x : A, hspace_op x pt = x &
hspace_left_identity pt = hspace_right_identity pt}}}
  apply equiv_functor_sigma_id; intro mu.
H: Funext
A: pType
mu: A -> selfmaps A
{p : mu pt = pt &
{H : (fun x : A => ev A (mu x)) == idmap &
H pt = ap (ev A) p @ point_eq (ev A)}} <~>
{hspace_left_identity : forall y : A, mu pt y = y &
{hspace_right_identity : forall x : A, mu x pt = x &
hspace_left_identity pt = hspace_right_identity pt}}
  apply (equiv_functor_sigma' (equiv_apD10 _ _ _)); intro H1; cbn.
H: Funext
A: pType
mu: A -> selfmaps A
H1: mu pt = pt
{H : (fun x : A => mu x pt) == idmap &
H pt = ap (fun f : A -> A => f pt) H1 @ 1} <~>
{hspace_right_identity : forall x : A, mu x pt = x &
apD10 H1 pt = hspace_right_identity pt}
  apply equiv_functor_sigma_id; intro H2; cbn.
H: Funext
A: pType
mu: A -> selfmaps A
H1: mu pt = pt
H2: (fun x : A => mu x pt) == idmap
H2 pt = ap (fun f : A -> A => f pt) H1 @ 1 <~>
apD10 H1 pt = H2 pt
  refine (equiv_path_inverse _ _ oE _).
H: Funext
A: pType
mu: A -> selfmaps A
H1: mu pt = pt
H2: (fun x : A => mu x pt) == idmap
H2 pt = ap (fun f : A -> A => f pt) H1 @ 1 <~>
H2 pt = apD10 H1 pt
  apply equiv_concat_r.
H: Funext
A: pType
mu: A -> selfmaps A
H1: mu pt = pt
H2: (fun x : A => mu x pt) == idmap
ap (fun f : A -> A => f pt) H1 @ 1 = apD10 H1 pt
  apply concat_p1.
Defined.

(** Our next goal is to see that when [A] is a left-invertible H-space, then the fibration [ev A] is trivial. *)

(** This lemma says that the family [fun a => A ->* [A,a]] is trivial. *)
Lemma equiv_pmap_hspace `{Funext} {A : pType}
  (a : A) `{IsHSpace A} `{!IsEquiv (hspace_op a)}
  : (A ->* A) <~> (A ->* [A,a]).
H: Funext
A: pType
a: A
H0: IsHSpace A
IsEquiv0: IsEquiv (hspace_op a)
(A ->* A) <~> (A ->* [A, a])
Proof.
H: Funext
A: pType
a: A
H0: IsHSpace A
IsEquiv0: IsEquiv (hspace_op a)
(A ->* A) <~> (A ->* [A, a])
  napply pequiv_pequiv_postcompose.
H: Funext
A: pType
a: A
H0: IsHSpace A
IsEquiv0: IsEquiv (hspace_op a)
A <~>* [A, a]
  rapply pequiv_hspace_left_op.
Defined.

(** The lemma gives us an equivalence on the total spaces (domains) of [ev A] and [psnd] (the projection out of the displayed product). *)
Proposition equiv_map_pmap_hspace `{Funext} {A : pType}
  `{IsHSpace A} `{forall a:A, IsEquiv (a *.)}
  : (A ->* A) * A <~> (A -> A).
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
(A ->* A) * A <~> (A -> A)
Proof.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
(A ->* A) * A <~> (A -> A)
  transitivity {a : A  & {f : A -> A & f pt = a}}.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
(A ->* A) * A <~> {a : A & {f : A -> A & f pt = a}}
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
{a : A & {f : A -> A & f pt = a}} <~> (A -> A)
  2: exact (equiv_sigma_contr _ oE (equiv_sigma_symm _)^-1%equiv).
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
(A ->* A) * A <~> {a : A & {f : A -> A & f pt = a}}
  refine (_ oE (equiv_sigma_prod0 _ _)^-1%equiv oE equiv_prod_symm _ _).
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
{_ : A & A ->* A} <~>
{a : A & {f : A -> A & f pt = a}}
  apply equiv_functor_sigma_id; intro a.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
a: A
(A ->* A) <~> {f : A -> A & f pt = a}
  exact ((issig_pmap A [A,a])^-1%equiv oE equiv_pmap_hspace a).
Defined.

(** The above is a pointed equivalence. *)
Proposition pequiv_map_pmap_hspace `{Funext} {A : pType}
  `{IsHSpace A} `{forall a:A, IsEquiv (a *.)}
  : [(A ->* A) * A, (pmap_idmap, pt)] <~>* selfmaps A.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
[(A ->* A) * A, (pmap_idmap, pt)] <~>* selfmaps A
Proof.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
[(A ->* A) * A, (pmap_idmap, pt)] <~>* selfmaps A
  snapply Build_pEquiv'.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
[(A ->* A) * A, (pmap_idmap, pt)] <~> selfmaps A
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
?f pt = pt
  1: exact equiv_map_pmap_hspace.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
equiv_map_pmap_hspace pt = pt
  cbn.
H: Funext
A: pType
H0: IsHSpace A
H1: forall a : A, IsEquiv (sg_op a)
(fun x : A => pt * x) = idmap
  apply path_forall, hspace_left_identity.
Defined.

(** When [A] is coherent, the pointed equivalence [pequiv_map_pmap_hspace] is a pointed equivalence over [A], i.e., a trivialization of [ev A]. *)
Proposition hspace_ev_trivialization `{Funext} {A : pType}
  `{IsCoherent A} `{forall a:A, IsEquiv (a *.)}
  : ev A o* pequiv_map_pmap_hspace ==* psnd (A:=[A ->* A, pmap_idmap]).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
ev A o* pequiv_map_pmap_hspace ==* psnd
Proof.
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
ev A o* pequiv_map_pmap_hspace ==* psnd
  snapply Build_pHomotopy.
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
ev A o* pequiv_map_pmap_hspace == psnd
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
?p pt =
dpoint_eq (ev A o* pequiv_map_pmap_hspace) @
(dpoint_eq psnd)^
  {
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
ev A o* pequiv_map_pmap_hspace == psnd intros [f x]; cbn.
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
f: A ->* A
x: A
x * f pt = x
    exact (ap _ (dpoint_eq f) @ hspace_right_identity _). }
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
((fun x0 : [(A ->* A) * A, (pmap_idmap, pt)] =>
  (fun (f : A ->* A) (x : A) =>
   ap (hspace_op x) (dpoint_eq f) @
   hspace_right_identity x
   :
   (ev A o* pequiv_map_pmap_hspace) (f, x) =
   psnd (f, x)) (fst x0) (snd x0))
 :
 ev A o* pequiv_map_pmap_hspace == psnd) pt =
dpoint_eq (ev A o* pequiv_map_pmap_hspace) @
(dpoint_eq psnd)^
  cbn.
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
1 @ hspace_right_identity pt =
(ap (fun f : A -> A => f pt)
   (path_forall (fun x : A => pt * x) idmap
      hspace_left_identity) @ 1) @ 1
  refine (concat_1p _ @ _^).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
(ap (fun f : A -> A => f pt)
   (path_forall (fun x : A => pt * x) idmap
      hspace_left_identity) @ 1) @ 1 =
hspace_right_identity pt
  refine (concat_p1 _ @ concat_p1 _ @ _).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
ap (fun f : A -> A => f pt)
  (path_forall (fun x : A => pt * x) idmap
     hspace_left_identity) = hspace_right_identity pt
  refine (ap10_path_forall _ _ _ _ @ _).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (sg_op a)
hspace_left_identity pt = hspace_right_identity pt
  exact iscoherent.
Defined.

(** ** The equivalence [IsCohHSpace A <~> (A ->* (A ->** A))] *)

Theorem equiv_cohhspace_ppmap `{Funext} {A : pType}
  `{IsCoherent A} `{forall a:A, IsEquiv (hspace_op a)}
  : IsCohHSpace A <~> (A ->* (A ->** A)).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (hspace_op a)
IsCohHSpace A <~> (A ->* (A ->** A))
Proof.
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (hspace_op a)
IsCohHSpace A <~> (A ->* (A ->** A))
  refine (_ oE equiv_iscohhspace_psect A).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (hspace_op a)
pSect (ev A) <~> (A ->* (A ->** A))
  refine (_ oE (equiv_pequiv_pslice_psect _ _ _ hspace_ev_trivialization^*)^-1%equiv).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (hspace_op a)
pSect psnd <~> (A ->* (A ->** A))
  refine (_ oE equiv_psect_psnd (A:=[A ->* A, pmap_idmap])).
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (hspace_op a)
(A ->* [A ->* A, pmap_idmap]) <~> (A ->* (A ->** A))
  refine (pequiv_pequiv_postcompose _); symmetry.
H: Funext
A: pType
H0: IsHSpace A
H1: IsCoherent A
H2: forall a : A, IsEquiv (hspace_op a)
(A ->** A) <~>* [A ->* A, pmap_idmap]
  rapply pequiv_hspace_left_op.
Defined.

(** Here is a third characterization of the type of coherent H-space structures. It simply involves shuffling the data around and using [Funext]. *)
Definition equiv_iscohhspace_ptd_action `{Funext} (A : pType)
  : IsCohHSpace A <~> { act : forall a, A ->* [A,a] & act pt ==* pmap_idmap }.
H: Funext
A: pType
IsCohHSpace A <~>
{act : forall a : IsPointed A, A ->* [A, a] &
act pt ==* pmap_idmap}
Proof.
H: Funext
A: pType
IsCohHSpace A <~>
{act : forall a : IsPointed A, A ->* [A, a] &
act pt ==* pmap_idmap}
  refine (_ oE (issig_iscohhspace A)^-1).
H: Funext
A: pType
{hspace_op : SgOp A &
{hspace_left_identity : LeftIdentity hspace_op pt &
{hspace_right_identity : RightIdentity hspace_op pt &
hspace_left_identity pt = hspace_right_identity pt}}} <~>
{act : forall a : IsPointed A, A ->* [A, a] &
act pt ==* pmap_idmap}
  unfold IsPointed.
H: Funext
A: pType
{hspace_op : SgOp A &
{hspace_left_identity : LeftIdentity hspace_op pt &
{hspace_right_identity : RightIdentity hspace_op pt &
hspace_left_identity pt = hspace_right_identity pt}}} <~>
{act : forall a : A, A ->* [A, a] &
act pt ==* pmap_idmap}
  (* First we shuffle the data on the LHS to be of this form: *)
  equiv_via {s : {act : A -> (A -> A) & forall a, act a pt = a} & {h : s.1 pt == idmap & h pt = s.2 pt}}.
H: Funext
A: pType
{hspace_op : SgOp A &
{hspace_left_identity : LeftIdentity hspace_op pt &
{hspace_right_identity : RightIdentity hspace_op pt &
hspace_left_identity pt = hspace_right_identity pt}}} <~>
{s : {act : A -> A -> A & forall a : A, act a pt = a}
& {h : s.1 pt == idmap & h pt = s.2 pt}}
H: Funext
A: pType
{s : {act : A -> A -> A & forall a : A, act a pt = a}
& {h : s.1 pt == idmap & h pt = s.2 pt}} <~>
{act : forall a : A, A ->* [A, a] &
act pt ==* pmap_idmap}
  1: make_equiv.
H: Funext
A: pType
{s : {act : A -> A -> A & forall a : A, act a pt = a}
& {h : s.1 pt == idmap & h pt = s.2 pt}} <~>
{act : forall a : A, A ->* [A, a] &
act pt ==* pmap_idmap}
  (* Then we break up [->*] and [==*] on the RHS using issig lemmas, and handle a trailing [@ 1]. *)
  snapply equiv_functor_sigma'.
H: Funext
A: pType
{act : A -> A -> A & forall a : A, act a pt = a} <~>
(forall a : A, A ->* [A, a])
H: Funext
A: pType
forall
a : {act : A -> A -> A & forall a : A, act a pt = a},
(fun
   s : {act : A -> A -> A &
       forall a0 : A, act a0 pt = a0} =>
 {h : s.1 pt == idmap & h pt = s.2 pt}) a <~>
(fun act : forall a0 : A, A ->* [A, a0] =>
 act pt ==* pmap_idmap) (?f a)
  -
H: Funext
A: pType
{act : A -> A -> A & forall a : A, act a pt = a} <~>
(forall a : A, A ->* [A, a]) refine (equiv_functor_forall_id (fun a => issig_pmap A [A,a]) oE _).
H: Funext
A: pType
{act : A -> A -> A & forall a : A, act a pt = a} <~>
(forall a : IsPointed A, {f : A -> [A, a] & f pt = pt})
    unfold IsPointed.
H: Funext
A: pType
{act : A -> A -> A & forall a : A, act a pt = a} <~>
(forall a : A, {f : A -> [A, a] & f pt = pt})
    napply equiv_sig_coind.
  -
H: Funext
A: pType
forall
a : {act : A -> A -> A & forall a : A, act a pt = a},
(fun
   s : {act : A -> A -> A &
       forall a0 : A, act a0 pt = a0} =>
 {h : s.1 pt == idmap & h pt = s.2 pt}) a <~>
(fun act : forall a0 : A, A ->* [A, a0] =>
 act pt ==* pmap_idmap)
  ((equiv_functor_forall_id
      (fun a0 : IsPointed A => issig_pmap A [A, a0])
    oE (equiv_sig_coind (fun _ : A => A -> A)
          (fun (x : A) (f : A -> [A, x]) => f pt = pt)
        :
        {act : A -> A -> A &
        forall a0 : A, act a0 pt = a0} <~>
        (forall a0 : IsPointed A,
         {f : A -> [A, a0] & f pt = pt}))) a) cbn.
H: Funext
A: pType
forall
a : {act : A -> A -> A & forall a : A, act a pt = a},
{h : a.1 pt == idmap & h pt = a.2 pt} <~>
{| pointed_fun := a.1 pt; dpoint_eq := a.2 pt |} ==*
pmap_idmap
    intros [act p]; simpl.
H: Funext
A: pType
act: A -> A -> A
p: forall a : A, act a pt = a
{h : act pt == idmap & h pt = p pt} <~>
{| pointed_fun := act pt; dpoint_eq := p pt |} ==*
pmap_idmap
    refine (issig_phomotopy _ _ oE _); cbn.
H: Funext
A: pType
act: A -> A -> A
p: forall a : A, act a pt = a
{h : act pt == idmap & h pt = p pt} <~>
{p0 : act pt == idmap & p0 pt = p pt @ 1}
    apply equiv_functor_sigma_id; intro q.
H: Funext
A: pType
act: A -> A -> A
p: forall a : A, act a pt = a
q: act pt == idmap
q pt = p pt <~> q pt = p pt @ 1
    apply equiv_concat_r; symmetry; apply concat_p1.
Defined.

(** It follows that any homogeneous type is a coherent H-space.  This generalizes [ishspace_homogeneous]. *)
Definition iscohhspace_homogeneous `{Funext} {A : pType} `{IsHomogeneous A}
  : IsCohHSpace A.
H: Funext
A: pType
H0: IsHomogeneous A
IsCohHSpace A
Proof.
H: Funext
A: pType
H0: IsHomogeneous A
IsCohHSpace A
  apply (equiv_iscohhspace_ptd_action A)^-1.
H: Funext
A: pType
H0: IsHomogeneous A
{act : forall a : IsPointed A, A ->* [A, a] &
act pt ==* pmap_idmap}
  exists homogeneous_pt_id.
H: Funext
A: pType
H0: IsHomogeneous A
homogeneous_pt_id pt ==* pmap_idmap
  exact homogeneous_pt_id_beta.
Defined.

(** One can also show directly that the H-space structure defined by [ishspace_homogeneous] is coherent. This also avoids [Funext]. *)
Definition iscoherent_homogeneous {A : pType} `{IsHomogeneous A}
  : @IsCoherent A (ishspace_homogeneous).
A: pType
H: IsHomogeneous A
IsCoherent A
Proof.
A: pType
H: IsHomogeneous A
IsCoherent A
  unfold IsCoherent; cbn.
A: pType
H: IsHomogeneous A
eisretr (ishomogeneous pt) pt =
ap (ishomogeneous pt)
  (moveR_equiv_V pt pt (point_eq (ishomogeneous pt))^) @
point_eq (ishomogeneous pt)
  set (f := ishomogeneous pt).
A: pType
H: IsHomogeneous A
f:= ishomogeneous pt: A <~>* [A, pt]
eisretr (ishomogeneous pt) pt =
ap (ishomogeneous pt)
  (moveR_equiv_V pt pt (point_eq (ishomogeneous pt))^) @
point_eq (ishomogeneous pt)
  change (eisretr f pt = ap f (moveR_equiv_V pt pt (point_eq f)^) @ point_eq f).
A: pType
H: IsHomogeneous A
f:= ishomogeneous pt: A <~>* [A, pt]
eisretr f pt =
ap f (moveR_equiv_V pt pt (point_eq f)^) @ point_eq f
  rewrite <- (point_eq f).
A: pType
H: IsHomogeneous A
f:= ishomogeneous pt: A <~>* [A, pt]
eisretr f pt = ap f (moveR_equiv_V pt pt 1^) @ 1
  unfold moveR_equiv_V; simpl.
A: pType
H: IsHomogeneous A
f:= ishomogeneous pt: A <~>* [A, pt]
eisretr f pt = ap f (1 @ eissect f pt) @ 1
  rhs napply concat_p1.
A: pType
H: IsHomogeneous A
f:= ishomogeneous pt: A <~>* [A, pt]
eisretr f pt = ap f (1 @ eissect f pt)
  lhs napply (eisadj f).
A: pType
H: IsHomogeneous A
f:= ishomogeneous pt: A <~>* [A, pt]
ap f (eissect f pt) = ap f (1 @ eissect f pt)
  apply ap.
A: pType
H: IsHomogeneous A
f:= ishomogeneous pt: A <~>* [A, pt]
eissect f pt = 1 @ eissect f pt
  symmetry; apply concat_1p.
Defined.

(** Using either of these, we can "upgrade" any left-invertible H-space structure to a coherent one. This one has a prime because the direct proof below computes better. *)
Definition iscohhspace_hspace' (A : pType)
  `{IsHSpace A} `{forall a, IsEquiv (a *.)}
  : IsCohHSpace A.
A: pType
H: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
IsCohHSpace A
Proof.
A: pType
H: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
IsCohHSpace A
  snapply Build_IsCohHSpace.
A: pType
H: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
IsHSpace A
A: pType
H: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
IsCoherent A
  {
A: pType
H: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
IsHSpace A napply ishspace_homogeneous.
A: pType
H: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
IsHomogeneous A
    exact ishomogeneous_hspace. }
A: pType
H: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
IsCoherent A
  exact iscoherent_homogeneous.
Defined.

(** The new multiplication is homotopic to the original one.  Relative to this, we expect that one of the identity laws also agrees, but that the other does not. *)
Definition iscohhspace_hspace'_beta_mu `{Funext} (A : pType)
  {m : IsHSpace A} `{forall a, IsEquiv (a *.)}
  : @hspace_op A (@ishspace_cohhspace A (iscohhspace_hspace' A)) = @hspace_op A m.
H: Funext
A: pType
m: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
hspace_op = hspace_op
Proof.
H: Funext
A: pType
m: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
hspace_op = hspace_op
  cbn. (* [*], [sg_op] and [hspace_op] all denote the original operation. *)
H: Funext
A: pType
m: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
(fun a b : A => a * (sg_op pt)^-1 b) = hspace_op
  funext a b.
H: Funext
A: pType
m: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
a, b: A
a * (sg_op pt)^-1 b = hspace_op a b
  refine (ap (a *.) _).
H: Funext
A: pType
m: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
a, b: A
(sg_op pt)^-1 b = b
  apply moveR_equiv_V.
H: Funext
A: pType
m: IsHSpace A
H0: forall a : A, IsEquiv (sg_op a)
a, b: A
b = pt * b
  symmetry; apply left_identity.
Defined.

(** Here's a different proof that directly upgrades an H-space structure, leaving the multiplication and left-identity definitionally the same, but changing the right-identity. *)
Definition iscohhspace_hspace (A : pType)
  {m : IsHSpace A} `{forall a, IsEquiv (a *.)}
  : IsCohHSpace A.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
IsCohHSpace A
Proof.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
IsCohHSpace A
  snapply Build_IsCohHSpace.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
IsHSpace A
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
IsCoherent A
  1: snapply Build_IsHSpace.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
SgOp A
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
LeftIdentity ?hspace_op pt
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
RightIdentity ?hspace_op pt
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
IsCoherent A
  -
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
SgOp A exact (@hspace_op A m).
  -
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
LeftIdentity hspace_op pt exact (@hspace_left_identity A m).
  -
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
RightIdentity hspace_op pt intro a.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
a: A
hspace_op a pt = a
    lhs exact (ap (a *.) (hspace_right_identity pt))^.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
a: A
a * hspace_op pt pt = a
    lhs exact (ap (a *.) (hspace_left_identity pt)).
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
a: A
a * pt = a
    exact (hspace_right_identity a).
  -
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
IsCoherent A unfold IsCoherent; cbn.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
hspace_left_identity pt =
(ap (sg_op pt) (hspace_right_identity pt))^ @
(ap (sg_op pt) (hspace_left_identity pt) @
 hspace_right_identity pt)
    apply moveL_Vp.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
ap (sg_op pt) (hspace_right_identity pt) @
hspace_left_identity pt =
ap (sg_op pt) (hspace_left_identity pt) @
hspace_right_identity pt
    lhs napply concat_A1p.
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
hspace_left_identity (hspace_op pt pt) @
hspace_right_identity pt =
ap (sg_op pt) (hspace_left_identity pt) @
hspace_right_identity pt
    refine (_ @@ 1).
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
hspace_left_identity (hspace_op pt pt) =
ap (sg_op pt) (hspace_left_identity pt)
    apply (cancelR _ _ (hspace_left_identity pt)).
A: pType
m: IsHSpace A
H: forall a : A, IsEquiv (sg_op a)
hspace_left_identity (hspace_op pt pt) @
hspace_left_identity pt =
ap (sg_op pt) (hspace_left_identity pt) @
hspace_left_identity pt
    symmetry; apply concat_A1p.
Defined.