From HoTT Require Import Basics Types Pointed HSpace.Core HSpace.Coherent.From HoTT Require Import Basics Types Pointed HSpace.Core HSpace.Coherent.

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

(** * Pointwise H-space structures *)

(** Whenever [X] is an H-space, so is the type of maps into [X].  Note: When writing [f * g], Coq only finds this instance if [f] is explicitly in the pointed type [[Y -> X, const pt]]. *)
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]
Proof.
H: Funext
X: pType
Y: Type
H0: IsHSpace X
IsHSpace [Y -> X, const pt]
  snapply 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]]. *)
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; exact iscoherent.
Defined.

(** If [X] is left-invertible, so is [[Y -> X, const pt]]. *)
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.

(** The pointwise product of two pointed maps into an H-space. This is the operation underlying the H-space structure [ishspace_pmap] on [Y ->** X], but requires no coherence. *)
Definition sgop_pmap {X Y : pType} `{IsHSpace X} (f g : Y ->* X) : Y ->* X.
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
Y ->* X
Proof.
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
Y ->* X
  snapply Build_pMap.
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
Y -> X
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
?f pt = pt
  -
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
Y -> X exact (fun y => (f y) * (g y)).
  -
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
(fun y : Y => f y * g y) pt = pt cbn beta.
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
f pt * g pt = pt
    lhs napply (ap _ (point_eq g)).
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
f pt * pt = pt
    lhs napply (ap (.* pt) (point_eq f)).
X, Y: pType
H: IsHSpace X
f, g: Y ->* X
pt * pt = pt
    apply hspace_left_identity.
Defined.

(** The constant map is a left unit for the pointwise product; this needs no coherence. *)
Definition leftidentity_pmap {X Y : pType} `{IsHSpace X} (g : Y ->* X)
  : sgop_pmap pconst g ==* g.
X, Y: pType
H: IsHSpace X
g: Y ->* X
sgop_pmap pconst g ==* g
Proof.
X, Y: pType
H: IsHSpace X
g: Y ->* X
sgop_pmap pconst g ==* g
  snapply Build_pHomotopy.
X, Y: pType
H: IsHSpace X
g: Y ->* X
sgop_pmap pconst g == g
X, Y: pType
H: IsHSpace X
g: Y ->* X
?p pt = dpoint_eq (sgop_pmap pconst g) @ (dpoint_eq g)^
  -
X, Y: pType
H: IsHSpace X
g: Y ->* X
sgop_pmap pconst g == g intro y; cbn.
X, Y: pType
H: IsHSpace X
g: Y ->* X
y: Y
pt * g y = g y
    apply hspace_left_identity.
  -
X, Y: pType
H: IsHSpace X
g: Y ->* X
((fun y : Y => hspace_left_identity (g y) : sgop_pmap pconst g y = g y)
 :
 sgop_pmap pconst g == g) pt =
dpoint_eq (sgop_pmap pconst g) @ (dpoint_eq g)^ cbn.
X, Y: pType
H: IsHSpace X
g: Y ->* X
hspace_left_identity (g pt) =
(ap (sg_op pt) (point_eq g) @ (1 @ hspace_left_identity pt)) @ (dpoint_eq g)^
    apply moveL_pV.
X, Y: pType
H: IsHSpace X
g: Y ->* X
hspace_left_identity (g pt) @ dpoint_eq g =
ap (sg_op pt) (point_eq g) @ (1 @ hspace_left_identity pt)
    exact (1 @@ concat_1p _ @ concat_A1p _ _)^.
Defined.

(** The constant map is a right unit for the pointwise product; the base-point coherence forces [right_identity pt = left_identity pt], so this needs [X] coherent. *)
Definition rightidentity_pmap {X Y : pType} `{IsCoherent X} (f : Y ->* X)
  : sgop_pmap f pconst ==* f.
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
f: Y ->* X
sgop_pmap f pconst ==* f
Proof.
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
f: Y ->* X
sgop_pmap f pconst ==* f
  snapply Build_pHomotopy.
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
f: Y ->* X
sgop_pmap f pconst == f
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
f: Y ->* X
?p pt = dpoint_eq (sgop_pmap f pconst) @ (dpoint_eq f)^
  -
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
f: Y ->* X
sgop_pmap f pconst == f intro y; cbn.
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
f: Y ->* X
y: Y
f y * pt = f y
    apply hspace_right_identity.
  -
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
f: Y ->* X
((fun y : Y => hspace_right_identity (f y) : sgop_pmap f pconst y = f y)
 :
 sgop_pmap f pconst == f) pt =
dpoint_eq (sgop_pmap f pconst) @ (dpoint_eq f)^ pelim f; cbn.
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
hspace_right_identity pt = (1 @ (1 @ hspace_left_identity pt)) @ 1
    symmetry.
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
(1 @ (1 @ hspace_left_identity pt)) @ 1 = hspace_right_identity pt
    lhs napply (concat_p1 _ @ concat_1p _ @ concat_1p _).
X, Y: pType
H: IsHSpace X
H0: IsCoherent X
hspace_left_identity pt = hspace_right_identity pt
    exact iscoherent.
Defined.

(** For the type of pointed maps [Y ->** X], coherence of [X] is needed even to get a non-coherent H-space structure on [Y ->** X]. *)
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)
  snapply 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) exact sgop_pmap.
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
LeftIdentity sgop_pmap pt intro g; exact (path_pforall (leftidentity_pmap g)).
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
RightIdentity sgop_pmap pt intro f; exact (path_pforall (rightidentity_pmap f)).
Defined.

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
leftidentity_pmap pt = rightidentity_pmap pt
  apply path_pforall.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
leftidentity_pmap pt ==* rightidentity_pmap pt
  snapply Build_pHomotopy.
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
leftidentity_pmap pt == rightidentity_pmap pt
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
?p pt =
dpoint_eq (leftidentity_pmap pt) @ (dpoint_eq (rightidentity_pmap pt))^
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
leftidentity_pmap pt == rightidentity_pmap 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
    exact iscoherent.
  -
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
((fun y : Y => iscoherent : leftidentity_pmap pt y = rightidentity_pmap pt y)
 :
 leftidentity_pmap pt == rightidentity_pmap pt) pt =
dpoint_eq (leftidentity_pmap pt) @ (dpoint_eq (rightidentity_pmap 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)^)^
    generalize (hspace_left_identity pt).
H: Funext
X, Y: pType
H0: IsHSpace X
H1: IsCoherent X
forall (p : hspace_op pt pt = pt) (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 p [].
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)^)^
    by destruct p.
Defined.

(** Since [sgop_pmap] is defined pointwise, it commutes with precomposition. *)
Definition sgop_pmap_precompose {X Y W : pType} `{IsHSpace X}
  (f g : Y ->* X) (h : W ->* Y)
  : sgop_pmap f g o* h ==* sgop_pmap (f o* h) (g o* h).
X, Y, W: pType
H: IsHSpace X
f, g: Y ->* X
h: W ->* Y
sgop_pmap f g o* h ==* sgop_pmap (f o* h) (g o* h)
Proof.
X, Y, W: pType
H: IsHSpace X
f, g: Y ->* X
h: W ->* Y
sgop_pmap f g o* h ==* sgop_pmap (f o* h) (g o* h)
  snapply Build_pHomotopy.
X, Y, W: pType
H: IsHSpace X
f, g: Y ->* X
h: W ->* Y
sgop_pmap f g o* h == sgop_pmap (f o* h) (g o* h)
X, Y, W: pType
H: IsHSpace X
f, g: Y ->* X
h: W ->* Y
?p pt =
dpoint_eq (sgop_pmap f g o* h) @ (dpoint_eq (sgop_pmap (f o* h) (g o* h)))^
  -
X, Y, W: pType
H: IsHSpace X
f, g: Y ->* X
h: W ->* Y
sgop_pmap f g o* h == sgop_pmap (f o* h) (g o* h) reflexivity.
  -
X, Y, W: pType
H: IsHSpace X
f, g: Y ->* X
h: W ->* Y
(fun x0 : W => 1) pt =
dpoint_eq (sgop_pmap f g o* h) @ (dpoint_eq (sgop_pmap (f o* h) (g o* h)))^ pelim h f g; cbn.
X, Y, W: pType
H: IsHSpace X
1 =
(1 @ (1 @ (1 @ hspace_left_identity pt))) @
(1 @ (1 @ hspace_left_identity pt))^  symmetry; apply concat_pp_V.
Defined.

(** [sgop_pmap] respects pointed homotopy in each argument. *)
Definition sgop_pmap_phomotopy {X Y : pType} `{IsHSpace X}
  {f f' g g' : Y ->* X} (p : f ==* f') (q : g ==* g')
  : sgop_pmap f g ==* sgop_pmap f' g'.
X, Y: pType
H: IsHSpace X
f, f', g, g': Y ->* X
p: f ==* f'
q: g ==* g'
sgop_pmap f g ==* sgop_pmap f' g'
Proof.
X, Y: pType
H: IsHSpace X
f, f', g, g': Y ->* X
p: f ==* f'
q: g ==* g'
sgop_pmap f g ==* sgop_pmap f' g'
  snapply Build_pHomotopy.
X, Y: pType
H: IsHSpace X
f, f', g, g': Y ->* X
p: f ==* f'
q: g ==* g'
sgop_pmap f g == sgop_pmap f' g'
X, Y: pType
H: IsHSpace X
f, f', g, g': Y ->* X
p: f ==* f'
q: g ==* g'
?p pt = dpoint_eq (sgop_pmap f g) @ (dpoint_eq (sgop_pmap f' g'))^
  -
X, Y: pType
H: IsHSpace X
f, f', g, g': Y ->* X
p: f ==* f'
q: g ==* g'
sgop_pmap f g == sgop_pmap f' g' intro y; exact (ap011 sg_op (p y) (q y)).
  -
X, Y: pType
H: IsHSpace X
f, f', g, g': Y ->* X
p: f ==* f'
q: g ==* g'
((fun y : Y => ap011 sg_op (p y) (q y)) : sgop_pmap f g == sgop_pmap f' g')
  pt =
dpoint_eq (sgop_pmap f g) @ (dpoint_eq (sgop_pmap f' g'))^ pelim p f f' q g g'; cbn.
X, Y: pType
H: IsHSpace X
1 =
(1 @ (1 @ hspace_left_identity pt)) @ (1 @ (1 @ hspace_left_identity pt))^  symmetry; apply concat_pV.
Defined.

(** If the H-space structure on [X] is left-invertible, so is the one induced on [Y ->** X]. *)
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; snapply 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 = 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 (sg_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 (sg_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.