From HoTT Require Import Basics HSpace.Core Pointed.Core Pointed.Loops.From HoTT Require Import Basics HSpace.Core Pointed.Core Pointed.Loops.

Local Open Scope mc_mult_scope.
Local Open Scope pointed_scope.

(** ** Coherent H-space structures *)

(** An H-space is coherent when the left and right identities agree at the base point. *)

Class IsCoherent (X : pType) `{IsHSpace X} :=
  iscoherent : left_identity pt = right_identity pt.

Record IsCohHSpace (A : pType) := {
    ishspace_cohhspace :: IsHSpace A;
    iscoherent_cohhspace :: IsCoherent A;
  }.

Definition issig_iscohhspace (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 } } }
      <~> IsCohHSpace A
  := ltac:(make_equiv).

(** A type equivalent to a coherent H-space is a coherent H-space. *)
Definition iscohhspace_equiv_cohhspace {X Y : pType} `{IsCohHSpace Y} (f : X <~>* Y)
  : IsCohHSpace X.
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
IsCohHSpace X
Proof.
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
IsCohHSpace X
  snapply Build_IsCohHSpace.
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
IsHSpace X
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
IsCoherent X
  -
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
IsHSpace X rapply (ishspace_equiv_hspace f).
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
IsHSpace Y
    apply ishspace_cohhspace; assumption.
  -
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
IsCoherent X unfold IsCoherent; cbn.
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
ap f^-1
  (ap (fun y : Y => sg_op y (f pt)) (point_eq f) @ left_identity (f pt)) @
eissect f pt =
ap f^-1 (ap (sg_op (f pt)) (point_eq f) @ right_identity (f pt)) @
eissect f pt
    refine (_ @@ 1).
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
ap f^-1
  (ap (fun y : Y => sg_op y (f pt)) (point_eq f) @ left_identity (f pt)) =
ap f^-1 (ap (sg_op (f pt)) (point_eq f) @ right_identity (f pt))
    refine (ap (ap f^-1) _).
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X <~>* Y
ap (fun y : Y => sg_op y (f pt)) (point_eq f) @ left_identity (f pt) =
ap (sg_op (f pt)) (point_eq f) @ right_identity (f pt)
    pelim f.
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X -> Y
iseq: IsEquiv f
ap (fun y : Y => sg_op y pt) 1 @ left_identity pt =
ap (sg_op pt) 1 @ right_identity pt
    refine (1 @@ _).
X, Y: pType
IsCohHSpace0: IsCohHSpace Y
f: X -> Y
iseq: IsEquiv f
left_identity pt = right_identity pt
    exact iscoherent.
Defined.

(** Every loop space is a coherent H-space. *)
Definition iscohhspace_loops {X : pType} : IsCohHSpace (loops X).
X: pType
IsCohHSpace (loops X)
Proof.
X: pType
IsCohHSpace (loops X)
  srapply Build_IsCohHSpace.
X: pType
IsHSpace (loops X)
X: pType
IsCoherent (loops X)
  -
X: pType
IsHSpace (loops X) exact ishspace_loops.
  -
X: pType
IsCoherent (loops X) reflexivity.
Defined.