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

Local Open Scope pointed_scope.
Local Open Scope mc_mult_scope.

(** * Pointwise H-space structures *)

(** Whenever [X] is an H-space, so is the type of maps into [X]. *)
Global Instance ishspace_map `{Funext} (X : pType) (Y : Type)
  `{IsHSpace X} : IsHSpace [Y -> X, const pt].
H: Funext
X: pType
Y: Type
H0: IsHSpace X
IsHSpace [Y -> X, const pt]
(* Note: When writing [f * g], Coq only finds this instance if [f] is explicitly in the pointed type [[Y -> X, const pt]]. *)
Proof.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
IsHSpace [Y -> X, const pt]
  snrapply Build_IsHSpace.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
SgOp [Y -> X, const pt]
H: Funext
X: pType
Y: Type
H0: IsHSpace X
LeftIdentity ?hspace_op pt
H: Funext
X: pType
Y: Type
H0: IsHSpace X
RightIdentity ?hspace_op pt
  -
H: Funext
X: pType
Y: Type
H0: IsHSpace X
SgOp [Y -> X, const pt] exact (fun f g y => (f y) * (g y)).
  -
H: Funext
X: pType
Y: Type
H0: IsHSpace X
LeftIdentity
  (fun (f g : [Y -> X, const pt]) (y : Y) => f y * g y)
  pt intro g; funext y.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
g: [Y -> X, const pt]
y: Y
pt y * g y = g y
    apply hspace_left_identity.
  -
H: Funext
X: pType
Y: Type
H0: IsHSpace X
RightIdentity
  (fun (f g : [Y -> X, const pt]) (y : Y) => f y * g y)
  pt intro f; funext y.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
f: [Y -> X, const pt]
y: Y
f y * pt y = f y
    apply hspace_right_identity.
Defined.

(** If [X] is coherent, so is [[Y -> X, const pt]]. *)
Global Instance iscoherent_ishspace_map `{Funext} (X : pType) (Y : Type)
  `{IsCoherent X} : IsCoherent [Y -> X, const pt].
H: Funext
X: pType
Y: Type
H0: IsHSpace X
H1: IsCoherent X
IsCoherent [Y -> X, const pt]
Proof.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
H1: IsCoherent X
IsCoherent [Y -> X, const pt]
  hnf; cbn.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
H1: IsCoherent X
path_forall (fun y : Y => const pt y * const pt y)
  (const pt)
  (fun y : Y => hspace_left_identity (const pt y)) =
path_forall (fun y : Y => const pt y * const pt y)
  (const pt)
  (fun y : Y => hspace_right_identity (const pt y))
  refine (ap _ _).
H: Funext
X: pType
Y: Type
H0: IsHSpace X
H1: IsCoherent X
(fun y : Y => hspace_left_identity (const pt y)) =
(fun y : Y => hspace_right_identity (const pt y))
  funext y; apply iscoherent.
Defined.

(** If [X] is left-invertible, so is [[Y -> X, const pt]]. *)
Global Instance isleftinvertible_hspace_map `{Funext} (X : pType) (Y : Type)
  `{IsHSpace X} `{forall x, IsEquiv (x *.)}
  : forall f : [Y -> X, const pt], IsEquiv (f *.).
H: Funext
X: pType
Y: Type
H0: IsHSpace X
H1: forall x : X, IsEquiv (sg_op x)
forall f : [Y -> X, const pt], IsEquiv (sg_op f)
Proof.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
H1: forall x : X, IsEquiv (sg_op x)
forall f : [Y -> X, const pt], IsEquiv (sg_op f)
  intro f; cbn.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
H1: forall x : X, IsEquiv (sg_op x)
f: [Y -> X, const pt]
IsEquiv (fun (g : Y -> X) (y : Y) => f y * g y)
  (** Left multiplication by [f] unifies with [functor_forall]. *)
  exact (isequiv_functor_forall (P:=const X) (f:=idmap)
           (g:=fun y gy => (f y) * gy)).
Defined.


(** For the type of pointed maps [Y ->** X], coherence of [X] is needed even to get a noncoherent H-space structure on [Y ->** X]. *)
Global Instance ishspace_pmap `{Funext} (X Y : pType) `{IsCoherent X}
  : IsHSpace (Y ->** X).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
IsHSpace (Y ->** X)
Proof.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
IsHSpace (Y ->** X)
  snrapply Build_IsHSpace.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
SgOp (Y ->** X)
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
LeftIdentity ?hspace_op pt
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
RightIdentity ?hspace_op pt
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
SgOp (Y ->** X) intros f g.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
Y ->** X
    snrapply Build_pMap.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
Y -> X
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
?Goal pt = pt
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
Y -> X exact (fun y => hspace_op (f y) (g y)).
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
(fun y : Y => hspace_op (f y) (g y)) pt = pt cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
hspace_op (f pt) (g pt) = pt
      refine (ap _ (point_eq g) @ _); cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
hspace_op (f pt) pt = pt
      refine (ap (.* pt) (point_eq f) @ _).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f, g: Y ->** X
pt * pt = pt
      apply hspace_left_identity.
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
LeftIdentity
  ((fun f g : Y ->** X =>
    Build_pMap Y X
      (fun y : Y => hspace_op (f y) (g y))
      (ap (hspace_op (f pt)) (point_eq g) @
       (ap (fun y : pfam_const X pt => y * pt)
          (point_eq f) @ hspace_left_identity pt
        :
        hspace_op (f pt) pt = pt)
       :
       (fun y : Y => hspace_op (f y) (g y)) pt = pt))
   :
   SgOp (Y ->** X)) pt intro g.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (pt y) (g y))
  (ap (hspace_op (pt pt)) (point_eq g) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq pt) @ hspace_left_identity pt)) = g
    apply path_pforall.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (pt y) (g y))
  (ap (hspace_op (pt pt)) (point_eq g) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq pt) @ hspace_left_identity pt)) ==* g
    snrapply Build_pHomotopy.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (pt y) (g y))
  (ap (hspace_op (pt pt)) (point_eq g) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq pt) @ hspace_left_identity pt)) == g
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
?p pt =
dpoint_eq
  (Build_pMap Y X
     (fun y : Y => hspace_op (pt y) (g y))
     (ap (hspace_op (pt pt)) (point_eq g) @
      (ap (fun y : pfam_const X pt => y * pt)
         (point_eq pt) @ hspace_left_identity pt))) @
(dpoint_eq g)^
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (pt y) (g y))
  (ap (hspace_op (pt pt)) (point_eq g) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq pt) @ hspace_left_identity pt)) == g intro y; cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
y: Y
hspace_op pt (g y) = g y
      apply hspace_left_identity.
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
((fun y : Y =>
  hspace_left_identity (g y)
  :
  Build_pMap Y X
    (fun y0 : Y => hspace_op (pt y0) (g y0))
    (ap (hspace_op (pt pt)) (point_eq g) @
     (ap (fun y0 : pfam_const X pt => y0 * pt)
        (point_eq pt) @ hspace_left_identity pt)) y =
  g y)
 :
 Build_pMap Y X (fun y : Y => hspace_op (pt y) (g y))
   (ap (hspace_op (pt pt)) (point_eq g) @
    (ap (fun y : pfam_const X pt => y * pt)
       (point_eq pt) @ hspace_left_identity pt)) == g)
  pt =
dpoint_eq
  (Build_pMap Y X
     (fun y : Y => hspace_op (pt y) (g y))
     (ap (hspace_op (pt pt)) (point_eq g) @
      (ap (fun y : pfam_const X pt => y * pt)
         (point_eq pt) @ hspace_left_identity pt))) @
(dpoint_eq g)^ cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
hspace_left_identity (g pt) =
(ap (hspace_op pt) (point_eq g) @
 (1 @ hspace_left_identity pt)) @ (dpoint_eq g)^
      apply moveL_pV.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
g: Y ->** X
hspace_left_identity (g pt) @ dpoint_eq g =
ap (hspace_op pt) (point_eq g) @
(1 @ hspace_left_identity pt)
      exact (1 @@ concat_1p _ @ concat_A1p _ _)^.
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
RightIdentity
  ((fun f g : Y ->** X =>
    Build_pMap Y X
      (fun y : Y => hspace_op (f y) (g y))
      (ap (hspace_op (f pt)) (point_eq g) @
       (ap (fun y : pfam_const X pt => y * pt)
          (point_eq f) @ hspace_left_identity pt
        :
        hspace_op (f pt) pt = pt)
       :
       (fun y : Y => hspace_op (f y) (g y)) pt = pt))
   :
   SgOp (Y ->** X)) pt intro f.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (f y) (pt y))
  (ap (hspace_op (f pt)) (point_eq pt) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq f) @ hspace_left_identity pt)) = f
    apply path_pforall.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (f y) (pt y))
  (ap (hspace_op (f pt)) (point_eq pt) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq f) @ hspace_left_identity pt)) ==* f
    snrapply Build_pHomotopy.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (f y) (pt y))
  (ap (hspace_op (f pt)) (point_eq pt) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq f) @ hspace_left_identity pt)) == f
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f: Y ->** X
?p pt =
dpoint_eq
  (Build_pMap Y X
     (fun y : Y => hspace_op (f y) (pt y))
     (ap (hspace_op (f pt)) (point_eq pt) @
      (ap (fun y : pfam_const X pt => y * pt)
         (point_eq f) @ hspace_left_identity pt))) @
(dpoint_eq f)^
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f: Y ->** X
Build_pMap Y X (fun y : Y => hspace_op (f y) (pt y))
  (ap (hspace_op (f pt)) (point_eq pt) @
   (ap (fun y : pfam_const X pt => y * pt)
      (point_eq f) @ hspace_left_identity pt)) == f intro y; cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f: Y ->** X
y: Y
hspace_op (f y) pt = f y
      apply hspace_right_identity.
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
f: Y ->** X
((fun y : Y =>
  hspace_right_identity (f y)
  :
  Build_pMap Y X
    (fun y0 : Y => hspace_op (f y0) (pt y0))
    (ap (hspace_op (f pt)) (point_eq pt) @
     (ap (fun y0 : pfam_const X pt => y0 * pt)
        (point_eq f) @ hspace_left_identity pt)) y =
  f y)
 :
 Build_pMap Y X (fun y : Y => hspace_op (f y) (pt y))
   (ap (hspace_op (f pt)) (point_eq pt) @
    (ap (fun y : pfam_const X pt => y * pt)
       (point_eq f) @ hspace_left_identity pt)) == f)
  pt =
dpoint_eq
  (Build_pMap Y X
     (fun y : Y => hspace_op (f y) (pt y))
     (ap (hspace_op (f pt)) (point_eq pt) @
      (ap (fun y : pfam_const X pt => y * pt)
         (point_eq f) @ hspace_left_identity pt))) @
(dpoint_eq f)^ pelim f; cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
hspace_right_identity pt =
(1 @ (1 @ hspace_left_identity pt)) @ 1
      symmetry.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
(1 @ (1 @ hspace_left_identity pt)) @ 1 =
hspace_right_identity pt
      lhs nrapply (concat_p1 _ @ concat_1p _ @ concat_1p _).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
hspace_left_identity pt = hspace_right_identity pt
      apply iscoherent.
Defined.

Global Instance iscoherent_hspace_pmap `{Funext} (X Y : pType) `{IsCoherent X}
  : IsCoherent (Y ->** X).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
IsCoherent (Y ->** X)
Proof.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
IsCoherent (Y ->** X)
  (* Note that [pt] sometimes means the constant map [Y ->* X]. *)
  unfold IsCoherent.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
left_identity pt = right_identity pt
  (* Both identities are created using [path_pforall]. *)
  refine (ap path_pforall _).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
Build_pHomotopy
  (fun y : Y => hspace_left_identity (pt y))
  (moveL_pV (dpoint_eq pt)
     (hspace_left_identity (pt pt))
     (ap (hspace_op pt) (point_eq pt) @
      (1 @ hspace_left_identity pt))
     ((1 @@ concat_1p (hspace_left_identity pt)) @
      concat_A1p hspace_left_identity (dpoint_eq pt))^) =
Build_pHomotopy
  (fun y : Y => hspace_right_identity (pt y))
  (paths_ind_r pt
     (fun (y : X) (p : y = pt) =>
      hspace_right_identity y =
      (1 @
       (ap (fun y0 : X => y0 * pt) p @
        hspace_left_identity pt)) @ p^)
     (((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
        concat_1p (1 @ hspace_left_identity pt)) @
       concat_1p (hspace_left_identity pt)) @
      iscoherent)^ (pt pt) (dpoint_eq pt))
  apply path_pforall.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
Build_pHomotopy
  (fun y : Y => hspace_left_identity (pt y))
  (moveL_pV (dpoint_eq pt)
     (hspace_left_identity (pt pt))
     (ap (hspace_op pt) (point_eq pt) @
      (1 @ hspace_left_identity pt))
     ((1 @@ concat_1p (hspace_left_identity pt)) @
      concat_A1p hspace_left_identity (dpoint_eq pt))^) ==*
Build_pHomotopy
  (fun y : Y => hspace_right_identity (pt y))
  (paths_ind_r pt
     (fun (y : X) (p : y = pt) =>
      hspace_right_identity y =
      (1 @
       (ap (fun y0 : X => y0 * pt) p @
        hspace_left_identity pt)) @ p^)
     (((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
        concat_1p (1 @ hspace_left_identity pt)) @
       concat_1p (hspace_left_identity pt)) @
      iscoherent)^ (pt pt) (dpoint_eq pt))
  snrapply Build_pHomotopy.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
Build_pHomotopy
  (fun y : Y => hspace_left_identity (pt y))
  (moveL_pV (dpoint_eq pt)
     (hspace_left_identity (pt pt))
     (ap (hspace_op pt) (point_eq pt) @
      (1 @ hspace_left_identity pt))
     ((1 @@ concat_1p (hspace_left_identity pt)) @
      concat_A1p hspace_left_identity (dpoint_eq pt))^) ==
Build_pHomotopy
  (fun y : Y => hspace_right_identity (pt y))
  (paths_ind_r pt
     (fun (y : X) (p : y = pt) =>
      hspace_right_identity y =
      (1 @
       (ap (fun y0 : X => y0 * pt) p @
        hspace_left_identity pt)) @ p^)
     (((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
        concat_1p (1 @ hspace_left_identity pt)) @
       concat_1p (hspace_left_identity pt)) @
      iscoherent)^ (pt pt) (dpoint_eq pt))
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
?p pt =
dpoint_eq
  (Build_pHomotopy
     (fun y : Y => hspace_left_identity (pt y))
     (moveL_pV (dpoint_eq pt)
        (hspace_left_identity (pt pt))
        (ap (hspace_op pt) (point_eq pt) @
         (1 @ hspace_left_identity pt))
        ((1 @@ concat_1p (hspace_left_identity pt)) @
         concat_A1p hspace_left_identity
           (dpoint_eq pt))^)) @
(dpoint_eq
   (Build_pHomotopy
      (fun y : Y => hspace_right_identity (pt y))
      (paths_ind_r pt
         (fun (y : X) (p : y = pt) =>
          hspace_right_identity y =
          (1 @
           (ap (fun y0 : X => y0 * pt) p @
            hspace_left_identity pt)) @ p^)
         (((concat_p1
              (1 @ (1 @ hspace_left_identity pt)) @
            concat_1p (1 @ hspace_left_identity pt)) @
           concat_1p (hspace_left_identity pt)) @
          iscoherent)^ (pt pt) (dpoint_eq pt))))^
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
Build_pHomotopy
  (fun y : Y => hspace_left_identity (pt y))
  (moveL_pV (dpoint_eq pt)
     (hspace_left_identity (pt pt))
     (ap (hspace_op pt) (point_eq pt) @
      (1 @ hspace_left_identity pt))
     ((1 @@ concat_1p (hspace_left_identity pt)) @
      concat_A1p hspace_left_identity (dpoint_eq pt))^) ==
Build_pHomotopy
  (fun y : Y => hspace_right_identity (pt y))
  (paths_ind_r pt
     (fun (y : X) (p : y = pt) =>
      hspace_right_identity y =
      (1 @
       (ap (fun y0 : X => y0 * pt) p @
        hspace_left_identity pt)) @ p^)
     (((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
        concat_1p (1 @ hspace_left_identity pt)) @
       concat_1p (hspace_left_identity pt)) @
      iscoherent)^ (pt pt) (dpoint_eq pt)) intro y; cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
y: Y
hspace_left_identity pt = hspace_right_identity pt
    apply iscoherent.
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
((fun y : Y =>
  iscoherent
  :
  Build_pHomotopy
    (fun y0 : Y => hspace_left_identity (pt y0))
    (moveL_pV (dpoint_eq pt)
       (hspace_left_identity (pt pt))
       (ap (hspace_op pt) (point_eq pt) @
        (1 @ hspace_left_identity pt))
       ((1 @@ concat_1p (hspace_left_identity pt)) @
        concat_A1p hspace_left_identity (dpoint_eq pt))^)
    y =
  Build_pHomotopy
    (fun y0 : Y => hspace_right_identity (pt y0))
    (paths_ind_r pt
       (fun (y0 : X) (p : y0 = pt) =>
        hspace_right_identity y0 =
        (1 @
         (ap (fun y1 : X => y1 * pt) p @
          hspace_left_identity pt)) @ p^)
       (((concat_p1
            (1 @ (1 @ hspace_left_identity pt)) @
          concat_1p (1 @ hspace_left_identity pt)) @
         concat_1p (hspace_left_identity pt)) @
        iscoherent)^ (pt pt) (dpoint_eq pt)) y)
 :
 Build_pHomotopy
   (fun y : Y => hspace_left_identity (pt y))
   (moveL_pV (dpoint_eq pt)
      (hspace_left_identity (pt pt))
      (ap (hspace_op pt) (point_eq pt) @
       (1 @ hspace_left_identity pt))
      ((1 @@ concat_1p (hspace_left_identity pt)) @
       concat_A1p hspace_left_identity (dpoint_eq pt))^) ==
 Build_pHomotopy
   (fun y : Y => hspace_right_identity (pt y))
   (paths_ind_r pt
      (fun (y : X) (p : y = pt) =>
       hspace_right_identity y =
       (1 @
        (ap (fun y0 : X => y0 * pt) p @
         hspace_left_identity pt)) @ p^)
      (((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
         concat_1p (1 @ hspace_left_identity pt)) @
        concat_1p (hspace_left_identity pt)) @
       iscoherent)^ (pt pt) (dpoint_eq pt))) pt =
dpoint_eq
  (Build_pHomotopy
     (fun y : Y => hspace_left_identity (pt y))
     (moveL_pV (dpoint_eq pt)
        (hspace_left_identity (pt pt))
        (ap (hspace_op pt) (point_eq pt) @
         (1 @ hspace_left_identity pt))
        ((1 @@ concat_1p (hspace_left_identity pt)) @
         concat_A1p hspace_left_identity
           (dpoint_eq pt))^)) @
(dpoint_eq
   (Build_pHomotopy
      (fun y : Y => hspace_right_identity (pt y))
      (paths_ind_r pt
         (fun (y : X) (p : y = pt) =>
          hspace_right_identity y =
          (1 @
           (ap (fun y0 : X => y0 * pt) p @
            hspace_left_identity pt)) @ p^)
         (((concat_p1
              (1 @ (1 @ hspace_left_identity pt)) @
            concat_1p (1 @ hspace_left_identity pt)) @
           concat_1p (hspace_left_identity pt)) @
          iscoherent)^ (pt pt) (dpoint_eq pt))))^ cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
iscoherent =
(((concat_p1 (hspace_left_identity pt))^ @
  ((1 @@ concat_1p (hspace_left_identity pt)) @
   concat_1p_p1 (hspace_left_identity pt))^) @
 (concat_p1 (1 @ (1 @ hspace_left_identity pt)))^) @
((((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
    concat_1p (1 @ hspace_left_identity pt)) @
   concat_1p (hspace_left_identity pt)) @ iscoherent)^)^
    generalize iscoherent as isc.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
forall isc : left_identity pt = right_identity pt,
isc =
(((concat_p1 (hspace_left_identity pt))^ @
  ((1 @@ concat_1p (hspace_left_identity pt)) @
   concat_1p_p1 (hspace_left_identity pt))^) @
 (concat_p1 (1 @ (1 @ hspace_left_identity pt)))^) @
((((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
    concat_1p (1 @ hspace_left_identity pt)) @
   concat_1p (hspace_left_identity pt)) @ isc)^)^
    unfold left_identity, right_identity.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
forall
isc : hspace_left_identity pt =
      hspace_right_identity pt,
isc =
(((concat_p1 (hspace_left_identity pt))^ @
  ((1 @@ concat_1p (hspace_left_identity pt)) @
   concat_1p_p1 (hspace_left_identity pt))^) @
 (concat_p1 (1 @ (1 @ hspace_left_identity pt)))^) @
((((concat_p1 (1 @ (1 @ hspace_left_identity pt)) @
    concat_1p (1 @ hspace_left_identity pt)) @
   concat_1p (hspace_left_identity pt)) @ isc)^)^
    (* The next line is essentially the same as [generalize], but for some reason that tactic doesn't work here. *)
    set (p := hspace_left_identity pt); clearbody p.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
p: hspace_op pt pt = pt
forall isc : p = hspace_right_identity pt,
isc =
(((concat_p1 p)^ @
  ((1 @@ concat_1p p) @ concat_1p_p1 p)^) @
 (concat_p1 (1 @ (1 @ p)))^) @
((((concat_p1 (1 @ (1 @ p)) @ concat_1p (1 @ p)) @
   concat_1p p) @ isc)^)^
    intros [].
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
p: hspace_op pt pt = pt
1 =
(((concat_p1 p)^ @
  ((1 @@ concat_1p p) @ concat_1p_p1 p)^) @
 (concat_p1 (1 @ (1 @ p)))^) @
((((concat_p1 (1 @ (1 @ p)) @ concat_1p (1 @ p)) @
   concat_1p p) @ 1)^)^
    induction p.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
1 =
(((concat_p1 1)^ @
  ((1 @@ concat_1p 1) @ concat_1p_p1 1)^) @
 (concat_p1 (1 @ (1 @ 1)))^) @
((((concat_p1 (1 @ (1 @ 1)) @ concat_1p (1 @ 1)) @
   concat_1p 1) @ 1)^)^
    reflexivity.
Defined.

(** If the H-space structure on [X] is left-invertible, so is the one induced on [Y ->** X]. *)
Global Instance isleftinvertible_hspace_pmap `{Funext} (X Y : pType)
  `{IsCoherent X} `{forall x, IsEquiv (x *.)}
  : forall f : Y ->** X, IsEquiv (f *.).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
forall f : Y ->** X, IsEquiv (sg_op f)
Proof.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
forall f : Y ->** X, IsEquiv (sg_op f)
  intro f.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
IsEquiv (sg_op f)
  srefine (isequiv_homotopic (equiv_functor_pforall_id _ _) _).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
forall a : Y, pfam_const X a <~> pfam_const X a
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
?f pt (dpoint (pfam_const X)) = dpoint (pfam_const X)
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
equiv_functor_pforall_id ?f ?p == sg_op f
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
forall a : Y, pfam_const X a <~> pfam_const X a exact (fun a => equiv_hspace_left_op (f a)).
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
(fun a : Y => equiv_hspace_left_op (f a)) pt
  (dpoint (pfam_const X)) = dpoint (pfam_const X) cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
f pt * pt = pt exact (right_identity _ @ point_eq f).
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
equiv_functor_pforall_id
  (fun a : Y => equiv_hspace_left_op (f a))
  (right_identity (f pt) @ point_eq f
   :
   (fun a : Y => equiv_hspace_left_op (f a)) pt
     (dpoint (pfam_const X)) = dpoint (pfam_const X)) ==
sg_op f intro g.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
equiv_functor_pforall_id
  (fun a : Y => equiv_hspace_left_op (f a))
  (right_identity (f pt) @ point_eq f) g = f * g
    apply path_pforall; snrapply Build_pHomotopy.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
equiv_functor_pforall_id
  (fun a : Y => equiv_hspace_left_op (f a))
  (right_identity (f pt) @ point_eq f) g == f * g
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
?p pt =
dpoint_eq
  (equiv_functor_pforall_id
     (fun a : Y => equiv_hspace_left_op (f a))
     (right_identity (f pt) @ point_eq f) g) @
(dpoint_eq (f * g))^
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
equiv_functor_pforall_id
  (fun a : Y => equiv_hspace_left_op (f a))
  (right_identity (f pt) @ point_eq f) g == f * g intro y; cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
y: Y
f y * g y = hspace_op (f y) (g y)
      reflexivity.
    +
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
((fun y : Y =>
  1
  :
  equiv_functor_pforall_id
    (fun a : Y => equiv_hspace_left_op (f a))
    (right_identity (f pt) @ point_eq f) g y =
  (f * g) y)
 :
 equiv_functor_pforall_id
   (fun a : Y => equiv_hspace_left_op (f a))
   (right_identity (f pt) @ point_eq f) g == f * g) pt =
dpoint_eq
  (equiv_functor_pforall_id
     (fun a : Y => equiv_hspace_left_op (f a))
     (right_identity (f pt) @ point_eq f) g) @
(dpoint_eq (f * g))^ cbn.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
1 =
(ap (sg_op (f pt)) (dpoint_eq g) @
 (right_identity (f pt) @ point_eq f)) @
(ap (hspace_op (f pt)) (point_eq g) @
 (ap (fun y : X => y * pt) (point_eq f) @
  hspace_left_identity pt))^ apply (moveR_1M _ _)^-1.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
ap (hspace_op (f pt)) (point_eq g) @
(ap (fun y : X => y * pt) (point_eq f) @
 hspace_left_identity pt) =
ap (sg_op (f pt)) (dpoint_eq g) @
(right_identity (f pt) @ point_eq f)
      apply whiskerL.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
ap (fun y : X => y * pt) (point_eq f) @
hspace_left_identity pt =
right_identity (f pt) @ point_eq f
      refine (whiskerL _ iscoherent @ _).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
H2: forall x : X, IsEquiv (sg_op x)
f: Y ->** X
g: Y ->* X
ap (fun y : X => y * pt) (point_eq f) @
right_identity pt = right_identity (f pt) @ point_eq f
      exact (concat_A1p right_identity (point_eq f)).
Defined.