diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 485e69938e9..110fcdecd2e 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -23,6 +23,11 @@ Record AbGroup := {
 Coercion abgroup_group : AbGroup >-> Group.
 Global Existing Instance abgroup_commutative.
 
+Definition Build_AbGroup' (G : Type) `(IsAbGroup G) : AbGroup := {|
+  abgroup_group := Build_Group G _ _ _ _;
+  abgroup_commutative := _;
+|}.
+
 Global Instance isabgroup_abgroup {A : AbGroup} : IsAbGroup A.
 Proof.
   split; exact _.
diff --git a/theories/Homotopy/Cohomology.v b/theories/Homotopy/Cohomology.v
new file mode 100644
index 00000000000..bc0f805081a
--- /dev/null
+++ b/theories/Homotopy/Cohomology.v
@@ -0,0 +1,51 @@
+Require Import Basics Types Pointed WildCat.Core WildCat.Equiv.
+Require Import Truncations.Core.
+Require Import Homotopy.EMSpace.
+Require Import Homotopy.HSpace.Core Homotopy.HSpace.Pointwise Homotopy.HSpace.HGroup Homotopy.HSpace.Coherent.
+Require Import Algebra.AbGroups.AbelianGroup.
+Require Import Homotopy.Suspension.
+Require Import Spheres HomotopyGroup.
+
+Local Open Scope pointed_scope.
+
+(** * Cohomology groups *)
+
+(** Reduced cohomology groups are defined as the homotopy classes of pointed maps from the space to an Eilenberg-MacLane space. The group structure comes from the H-space structure on [K(G, n)]. *)
+Definition Cohomology `{Univalence} (n : nat) (X : pType) (G : AbGroup) : AbGroup.
+Proof.
+  snrapply Build_AbGroup'.
+  1: exact (Tr 0 (X ->** K(G, n))).
+  1-3: shelve.
+  nrapply isabgroup_ishabgroup_tr.
+  nrapply ishabgroup_hspace_pmap. 
+  apply iscohhabgroup_em.
+Defined.
+
+(** ** Cohomology of suspension *)
+
+(** The (n+1)th cohomology of a suspension is the nth cohomology of the original space. *) 
+(* TODO: show this preserves the operation somehow and is therefore a group iso *)
+Definition cohomology_susp `{Univalence} n (X : pType) G
+  : Cohomology n.+1 (psusp X) G <~> Cohomology n X G.
+Proof.
+  apply Trunc_functor_equiv.
+  nrefine (_ oE (loop_susp_adjoint _ _)).
+  rapply pequiv_pequiv_postcompose.
+  symmetry.
+  apply pequiv_loops_em_em.
+Defined.
+
+(** ** Cohomology of spheres *)
+
+(* TODO: improve this to a group isomorphism once cohomology can be easily checked to be op preserving. *)
+Definition cohomology_sn `{Univalence} (n : nat) (G : AbGroup)
+  : Cohomology n.+1 (psphere n.+1) G <~> G.
+Proof.
+  nrefine (_ oE (equiv_tr 0 _)^-1).
+  1: refine ?[goal1].
+  2: { rapply istrunc_equiv_istrunc. symmetry. apply ?goal1. }
+  nrefine (_ oE pmap_from_psphere_iterated_loops _ _).
+  symmetry.
+  rapply pequiv_loops_em_g.
+Defined.
+  
\ No newline at end of file
diff --git a/theories/Homotopy/EMSpace.v b/theories/Homotopy/EMSpace.v
index a2f366558e2..7c33b6a78f4 100644
--- a/theories/Homotopy/EMSpace.v
+++ b/theories/Homotopy/EMSpace.v
@@ -103,5 +103,15 @@ Section EilenbergMacLane.
     2: apply pequiv_loops_em_em.
     apply iscohhspace_loops.
   Defined.
+  
+  Definition iscohhabgroup_em {G : AbGroup} (n : nat)
+    : IsCohHAbGroup K(G, n).
+  Proof.
+    nrapply iscohhabgroup_equiv_cohhabgroup.
+    2: apply pequiv_loops_em_em.
+    nrapply iscohhabgroup_equiv_cohhabgroup.
+    2: exact (emap loops (pequiv_loops_em_em _ _)).
+    apply iscohhabgroup_loops_loops.
+  Defined.
 
 End EilenbergMacLane.
diff --git a/theories/Homotopy/HSpace.v b/theories/Homotopy/HSpace.v
index 0f3d0c879e6..5b9179f4925 100644
--- a/theories/Homotopy/HSpace.v
+++ b/theories/Homotopy/HSpace.v
@@ -2,3 +2,5 @@ Require Export HSpace.Core.
 Require Export HSpace.Coherent.
 Require Export HSpace.Pointwise.
 Require Export HSpace.Moduli.
+Require Export HSpace.HGroup.
+
diff --git a/theories/Homotopy/HSpace/Coherent.v b/theories/Homotopy/HSpace/Coherent.v
index d2899cb8a47..d8566484b55 100644
--- a/theories/Homotopy/HSpace/Coherent.v
+++ b/theories/Homotopy/HSpace/Coherent.v
@@ -10,11 +10,10 @@ Local Open Scope pointed_scope.
 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;
-  }.
-#[export] Existing Instances ishspace_cohhspace iscoherent_cohhspace.
+Class IsCohHSpace (A : pType) := {
+  ishspace_cohhspace :: IsHSpace A;
+  iscoherent_cohhspace :: IsCoherent A;
+}.
 
 Definition issig_iscohhspace (A : pType)
   : { hspace_op : SgOp A
@@ -35,7 +34,6 @@ Definition iscohhspace_equiv_cohhspace {X Y : pType} `{IsCohHSpace Y} (f : X <~>
 Proof.
   snrapply Build_IsCohHSpace.
   - rapply (ishspace_equiv_hspace f).
-    apply ishspace_cohhspace; assumption.
   - unfold IsCoherent; cbn.
     refine (_ @@ 1).
     refine (ap (ap f^-1) _).
@@ -51,3 +49,328 @@ Proof.
   - apply ishspace_loops.
   - reflexivity.
 Defined.
+
+(** A 0-truncated H-space is a coherent H-space. *)
+Global Instance iscoherent_hset (X : pType) `{IsHSpace X} `{IsHSet X}
+  : IsCoherent X.
+Proof.
+  apply path_ishprop.
+Defined.
+
+(** A coherently associative H-space is a H-space in which the operation is associative together with an additional coherence. *)
+Class IsCohAssociative (X : pType) `{IsHSpace X} := {
+  associative_iscohassoc :: Associative (.*.);
+  associative_iscohassoc_coh : simple_associativity pt pt pt
+      = ap (pt *.) (left_identity pt) @ ap (.* pt) (left_identity pt)^;
+}.
+
+(** A 0-truncated H-space whose operation is associative is coherently associative. *)
+Global Instance iscohassoc_hset (X : pType) `{IsHSpace X} `{!Associative (.*.)} `{IsHSet X}
+  : IsCohAssociative X.
+Proof.
+  snrapply Build_IsCohAssociative.
+  1: exact _.
+  apply path_ishprop.
+Defined.
+
+(** A coherent H-monoid, also known as a coherent A_3-space, is a coherent H-space that is also coherently associative. *)
+Class IsCohHMonoid (A : pType) := {
+  iscohhspace_iscohhmonoid :: IsCohHSpace A;
+  iscohassoc_cohassochspace :: IsCohAssociative A;
+}.
+
+(** A type equivalent to a coherent H-monoid is a coherent H-monoid. *)
+Definition iscohhmonoid_equiv_cohmonoid {X Y : pType} `{IsCohHMonoid Y} (f : X <~>* Y)
+  : IsCohHMonoid X.
+Proof.
+  snrapply Build_IsCohHMonoid.
+  - rapply (iscohhspace_equiv_cohhspace f).
+  - snrapply Build_IsCohAssociative.
+    + intros x y z.
+      nrefine (ap f^-1 _).
+      lhs nrapply ap.
+      1: apply eisretr.
+      rhs nrapply (ap (.* _)).
+      2: apply eisretr.
+      apply associative_iscohassoc.
+    + unfold simple_associativity; cbn.
+      (** The path algebra is a little complicated but still straightforward. *)
+      rhs nrapply (_ @@ _).
+      2: { lhs nrefine (ap_compose (fun x => sg_op (f x) _) f^-1 _).
+        nrapply ap.
+        nrapply (ap_compose f (fun x => sg_op x _)). }
+      2: { lhs nrefine (ap_compose (fun x => sg_op _ (f x)) f^-1 _).
+        nrapply ap.
+        nrapply (ap_compose f (sg_op _)). }
+      rhs_V nrapply ap_pp.
+      nrapply ap.
+      rhs nrapply (ap _ _ @@ ap _ _).
+      2: lhs nrapply ap; [nrapply inv_pp|].
+      2,3: lhs nrapply ap_pp.
+      2: nrefine (1 @@ _).
+      3: nrefine (_ @@ 1).
+      2: lhs_V nrapply ap; [ apply ap_V | ].
+      2,3: lhs_V nrapply ap_compose.
+      2,3: nrapply (ap_homotopic (eisretr f)).
+      (** I gave up avoiding rewrite here. TODO: remove rewrite *)
+      rewrite eisadj.
+      rewrite 2 ap_idmap.
+      rewrite ap_V.
+      rewrite ? concat_pp_p.
+      rewrite concat_Vp.
+      rewrite ? concat_p_pp.
+      rewrite concat_Vp.
+      hott_simpl.
+      (** This is finally simple enough that we can use [pelim]. *)
+      pelim f.
+      simpl.
+      apply moveR_pV.
+      apply moveR_Mp.
+      lhs nrapply associative_iscohassoc_coh.
+      rewrite concat_1p, concat_p1.
+      apply moveL_Vp.
+      rhs nrapply concat_pp_p.
+      rewrite ap_pp.
+      rhs nrapply concat_pp_p.
+      f_ap. f_ap.
+      rewrite ap_pp.
+      rhs nrapply concat_pp_p.
+      rewrite ap_V.
+      apply moveL_Vp. 
+      rewrite concat_pV.
+      rewrite ap_V.
+      symmetry.
+      apply concat_Vp.
+Defined.
+
+Definition iscohhmonoid_loops {X : pType} : IsCohHMonoid (loops X).
+Proof.
+  snrapply Build_IsCohHMonoid.
+  - apply iscohhspace_loops.
+  - snrapply Build_IsCohAssociative.
+    + intros p q r.
+      apply concat_p_pp.
+    + reflexivity.
+Defined.
+
+(** A coherently commutative H-space is a H-space in which the operation is commutative together with an additional coherence. *)
+Class IsCohCommutative (X : pType) `{IsHSpace X} := {
+  commutative_iscohcommutative :: Commutative (.*.);
+  iscohcommutative : commutativity pt pt = 1;
+}.
+
+(** A 0-truncated H-space whose operation is commutative is coherently commutative. *)
+Global Instance iscohcommutative_hset (X : pType) `{IsHSpace X} `{!Commutative (.*.)} `{IsHSet X}
+  : IsCohCommutative X.
+Proof.
+  snrapply Build_IsCohCommutative.
+  1: exact _.
+  apply path_ishprop.
+Defined.
+
+(** A type equivalent to a H-space with a coherent commutative operation is a H-space with a coherent commutative operation. *)
+Definition iscohcommutative_equiv_cohcommutative {X Y : pType} `{IsCohCommutative Y} (f : X <~>* Y)
+  : @IsCohCommutative X (ishspace_equiv_hspace f).
+Proof.
+  snrapply Build_IsCohCommutative.
+  - intros x y.
+    nrefine (ap f^-1 _).
+    apply commutativity.
+  - unfold commutativity; cbn.
+    pelim f.
+    change (?x = _) with (x = ap f^-1 1).
+    nrapply ap.
+    apply iscohcommutative.
+Defined.
+
+Definition iscohcommutative_loops_loops {X : pType}
+  : @IsCohCommutative (loops (loops X)) ishspace_loops.
+Proof.
+  snrapply Build_IsCohCommutative.
+  - intros p q.
+    apply eckmann_hilton.
+  - reflexivity.
+Defined.
+
+(** A coherent H-commutative monoid is a coherent H-monoid that is also coherently commutative. This is not an E_3-space as it would also have to be an A_oo-space. *)
+Class IsCohHCommutativeMonoid (A : pType) := {
+  iscohhmonoid_iscohhcommutativemonoid :: IsCohHMonoid A;
+  iscohcommutative_cohcommutativemonoid :: IsCohCommutative A;
+}.
+
+(** A type equivalent to a coherent H-commutative monoid is a coherent H-commutative monoid. *)
+Definition iscohhcommutativemonoid_equiv_cohcommutativemonoid
+  {X Y : pType} `{IsCohHCommutativeMonoid Y} (f : X <~>* Y)
+  : IsCohHCommutativeMonoid X.
+Proof.
+  snrapply Build_IsCohHCommutativeMonoid.
+  - rapply (iscohhmonoid_equiv_cohmonoid f).
+  - rapply (iscohcommutative_equiv_cohcommutative f).
+Defined.
+
+Definition iscohcommutativemonoid_loops_loops {X : pType}
+  : IsCohHCommutativeMonoid (loops (loops X)).
+Proof.
+  snrapply Build_IsCohHCommutativeMonoid.
+  - apply iscohhmonoid_loops.
+  - apply iscohcommutative_loops_loops.
+Defined.
+
+(** A coherent H-group is a coherent H-space in which every element has an inverse in a coherent way. *)
+Class IsCohHGroup (A : pType) := {
+  iscohhmonoid_iscohhgroup :: IsCohHMonoid A;
+  negate_cohhgroup :: Negate A;
+  negate_coh : negate pt = pt;
+  left_inverse_cohhgroup :: LeftInverse (.*.) negate_cohhgroup pt;
+  left_inverse_coh : left_inverse pt = ap (.* pt) negate_coh @ hspace_left_identity pt;
+  right_inverse_cohhgroup :: RightInverse (.*.) negate_cohhgroup pt;
+  right_inverse_coh : right_inverse pt = ap (pt *.) negate_coh @ hspace_left_identity pt;
+}.
+
+(** A type equivalent to a coherent H-group is a coherent H-group. *)
+Definition iscohhgroup_equiv_cohhgroup {X Y : pType} `{IsCohHGroup Y} (f : X <~>* Y)
+  : IsCohHGroup X.
+Proof.
+  snrapply Build_IsCohHGroup.
+  - rapply (iscohhmonoid_equiv_cohmonoid f).
+  - intros x.
+    apply f^-1.
+    apply negate.
+    apply f.
+    exact x.
+  - unfold negate.
+    apply moveR_equiv_V.
+    refine (ap _ (point_eq f) @ _ @ (point_eq f)^).
+    apply negate_coh.
+  - intros x.
+    simpl.
+    unfold sg_op.
+    apply moveR_equiv_V.
+    lhs nrapply (ap (.* _)).
+    1: apply eisretr.
+    lhs apply left_inverse.
+    symmetry.
+    apply point_eq. 
+  - simpl.
+    (** TODO: Simplify this proof *) 
+    unfold moveR_equiv_V.
+    unfold left_inverse.
+    rhs nrapply concat_p_pp.
+    nrefine (_ @@ 1).
+    apply moveL_pM.
+    rewrite <- (ap_V f^-1).
+    rewrite <- (ap_pp f^-1).
+    unfold sg_op.
+    simpl.
+    symmetry.
+    nrefine (ap_compose (fun x => sg_op (f x) _) f^-1 _ @ _).
+    nrapply ap.
+    lhs nrapply (ap_pp ((.* _) o f)).
+    apply moveR_pM.
+    lhs nrapply (ap_compose f (.* _)).
+    lhs nrapply ap.
+    { lhs_V nrapply (ap_compose f^-1 f).
+      nrapply (ap_homotopic (eisretr f)). }
+    rewrite ap_idmap.
+    rewrite ap_pp.
+    f_ap.
+    { rewrite ap_pp.
+      rhs nrapply concat_pp_p.
+      f_ap.
+      rewrite ap_pp.
+      apply moveL_pV.
+      pelim f.
+      simpl.
+      hott_simpl.
+      symmetry.
+      apply left_inverse_coh. }
+    lhs nrapply (ap_V (.* _)).
+    apply inverse2.
+    rhs nrapply (ap_compose f (.* _)).
+    apply ap.
+    apply eisadj.
+  - intros x.
+    simpl.
+    unfold sg_op.
+    apply moveR_equiv_V.
+    lhs nrapply (ap (_ *.)).
+    1: apply eisretr.
+    lhs apply right_inverse.
+    symmetry.
+    apply point_eq.
+  - simpl.
+    (** TODO: simplify proof *)
+    unfold moveR_equiv_V.
+    unfold right_inverse.
+    rhs nrapply concat_p_pp.
+    nrefine (_ @@ 1).
+    apply moveL_pM.
+    rewrite <- (ap_V f^-1).
+    rewrite <- (ap_pp f^-1).
+    unfold sg_op.
+    simpl.
+    symmetry.
+    nrefine (ap_compose (fun x => sg_op _ (f x)) f^-1 _ @ _).
+    nrapply ap.
+    lhs nrapply (ap_pp (sg_op _ o f)).
+    apply moveR_pM.
+    lhs nrapply (ap_compose f (sg_op _)).
+    lhs nrapply ap.
+    { lhs_V nrapply (ap_compose f^-1 f).
+      nrapply (ap_homotopic (eisretr f)). }
+    rewrite ap_idmap.
+    rewrite ap_pp.
+    f_ap.
+    { rewrite ap_pp.
+      rhs nrapply concat_pp_p.
+      f_ap.
+      rewrite ap_pp.
+      apply moveL_pV.
+      pelim f.
+      simpl.
+      hott_simpl.
+      symmetry.
+      apply right_inverse_coh. }
+    lhs nrapply (ap_V (_ *.)).
+    apply inverse2.
+    rhs nrapply (ap_compose f (sg_op _)).
+    apply ap.
+    apply eisadj.
+Defined.
+
+Definition iscohgroup_loops {X : pType} : IsCohHGroup (loops X).
+Proof.
+  snrapply Build_IsCohHGroup.
+  - apply iscohhmonoid_loops.
+  - intros p.
+    exact p^.
+  - reflexivity.
+  - intros p.
+    apply concat_Vp.
+  - reflexivity.
+  - intros p.
+    apply concat_pV.
+  - reflexivity.
+Defined.
+
+(** A coherent H-Abelian group is a coherent H-group in which the operation is commutative. *)
+Class IsCohHAbGroup (A : pType) := {
+  iscohgroup_cohabgroup :: IsCohHGroup A;
+  commutative_cohabgroup :: IsCohCommutative A;
+}.
+
+(** A type equivalent to a coherent H-Abelian group is a coherent H-Abelian group. *)
+Definition iscohhabgroup_equiv_cohhabgroup {X Y : pType} `{IsCohHAbGroup Y} (f : X <~>* Y)
+  : IsCohHAbGroup X.
+Proof.
+  snrapply Build_IsCohHAbGroup.
+  - rapply (iscohhgroup_equiv_cohhgroup f).
+  - rapply (iscohcommutative_equiv_cohcommutative f).
+Defined.
+
+Definition iscohhabgroup_loops_loops {X : pType} : IsCohHAbGroup (loops (loops X)).
+Proof.
+  snrapply Build_IsCohHAbGroup.
+  - apply iscohgroup_loops.
+  - apply iscohcommutative_loops_loops.
+Defined.
diff --git a/theories/Homotopy/HSpace/HGroup.v b/theories/Homotopy/HSpace/HGroup.v
new file mode 100644
index 00000000000..eebd917c96e
--- /dev/null
+++ b/theories/Homotopy/HSpace/HGroup.v
@@ -0,0 +1,114 @@
+Require Import Basics Types.
+Require Import Pointed.Core HSpace.Core Truncations.Core abstract_algebra.
+
+Local Open Scope pointed_scope.
+Local Open Scope mc_mult_scope.
+
+(** A H-monoid is a H-space with an associative binary operation. *)
+Class IsHMonoid (X : pType) := {
+  ishspace_ishmonoid :: IsHSpace X;
+  assoc_ishmonoid :: Associative (.*.);
+}.
+
+(** A H-commutative monoid is a H-space with an associative and commutative binary operation. *)
+Class IsHCommutativeMonoid (X : pType) := {
+  ishmonoid_ishcommutativemonoid :: IsHMonoid X;
+  comm_ishcomutativemonoid :: Commutative (.*.);
+}.
+  
+(** A H-group is a H-space with an associative binary operation an inversion. *)
+Class IsHGroup (X : pType) := {
+  ishmonoid_ishgroup :: IsHMonoid X;
+  negate_ishgroup :: Negate X;
+  left_inverse_ishgroup :: LeftInverse (.*.) (-) pt;
+  right_inverse_ishgroup :: RightInverse (.*.) (-) pt;
+}.
+
+(** A H-abelian group is a H-space with an associative and commutative binary operation and invertible left and right multiplication. *)
+Class IsHAbGroup (X : pType) := {
+  ishgroup_ishabeliangroup :: IsHGroup X;
+  comm_ishabeliangroup :: Commutative (.*.);
+}.
+
+(** The 0-truncation of a space with an operation has a truncated version of that operation. *)
+Local Instance sgop_tr X `{SgOp X} : SgOp (Tr 0 X).
+Proof.
+  intros x y.
+  strip_truncations.
+  apply tr.
+  exact (x * y).
+Defined.  
+
+(** The 0-truncation of a space with unit has a truncated unit. *)
+Local Instance monoid_unit_tr X `{MonUnit X} : MonUnit (Tr 0 X).
+Proof.
+  apply tr.
+  exact mon_unit.
+Defined.
+
+(** The 0-truncation of a H-monoid is a monoid. *)
+Global Instance ismonoid_ishmonoid_tr X `{IsHMonoid X} : IsMonoid (Tr 0 X).
+Proof.
+  repeat split.
+  1: exact _.
+  - intros x y z.
+    strip_truncations.
+    apply (ap tr).
+    apply assoc_ishmonoid.
+  - intros x.
+    strip_truncations.
+    apply (ap tr).
+    apply left_identity.
+  - intros x.
+    strip_truncations.
+    apply (ap tr).
+    apply right_identity.
+Defined.
+
+(** The 0-truncation of a H-commutative monoid is a commutative monoid. *)
+Local Instance iscommutativemonoid_ishcommutativemonoid_tr X `{IsHCommutativeMonoid X}
+  : IsCommutativeMonoid (Tr 0 X).
+Proof.
+  split.
+  1: exact _.
+  intros x y.
+  strip_truncations.
+  apply (ap tr).
+  apply (comm_ishcomutativemonoid x y).
+Defined.
+
+(** The 0-truncation of a space with invertible left and right multiplication has a negation. *)
+Local Instance neg_tr X `{Negate X} : Negate (Tr 0 X).
+Proof.
+  intros x.
+  strip_truncations.
+  apply tr.
+  exact (- x).
+Defined.
+
+(** The 0-truncation of a H-group is a group. *)
+Global Instance isgroup_ishgroup_tr X `{IsHGroup X} : IsGroup (Tr 0 X).
+Proof.
+  split.
+  1: exact _.
+  - intros x.
+    strip_truncations.
+    apply (ap tr).
+    rapply left_inverse.
+  - intros x.
+    strip_truncations.
+    apply (ap tr).
+    rapply right_inverse.
+Defined.
+
+(** The 0-truncation of a H-abelian group is an abelian group. *)
+Global Instance isabgroup_ishabgroup_tr X `{IsHAbGroup X}
+  : IsAbGroup (Tr 0 X).
+Proof.
+  split.
+  1: exact _.
+  intros x y.
+  strip_truncations.
+  apply (ap tr).
+  apply (comm_ishabeliangroup x y).
+Defined.
diff --git a/theories/Homotopy/HSpace/Pointwise.v b/theories/Homotopy/HSpace/Pointwise.v
index fa82754c666..4cb1eea54a6 100644
--- a/theories/Homotopy/HSpace/Pointwise.v
+++ b/theories/Homotopy/HSpace/Pointwise.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Pointed HSpace.Core HSpace.Coherent.
+Require Import Basics Types Pointed HSpace.Core HSpace.Coherent HSpace.HGroup.
 
 Local Open Scope pointed_scope.
 Local Open Scope mc_mult_scope.
@@ -38,7 +38,6 @@ Proof.
            (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).
@@ -109,3 +108,102 @@ Proof.
       refine (whiskerL _ iscoherent @ _).
       exact (concat_A1p right_identity (point_eq f)).
 Defined.
+
+(** If the H-space structure on [X] is right-invertible, so is the one induced on [Y ->** X]. *)
+Global Instance isrightinvertible_hspace_pmap `{Funext} (X Y : pType)
+  `{IsCoherent X} `{forall x, IsEquiv (.* x)}
+  : forall f : Y ->** X, IsEquiv (.* f).
+Proof.
+  intro f.
+  srefine (isequiv_homotopic (equiv_functor_pforall_id _ _) _).
+  - exact (fun a => equiv_hspace_right_op (f a)).
+  - cbn. exact (left_identity _ @ point_eq f).
+  - intro g.
+    apply path_pforall; snrapply Build_pHomotopy.
+    + intro y; cbn.
+      reflexivity.
+    + cbn. apply (moveR_1M _ _)^-1.
+      pelim f g.
+      simpl.
+      nrapply whiskerL.
+      apply concat_1p_p1.
+Defined.
+
+(** If the H-space structure on [X] is coherently commutative, then the H-space structure on [Y ->** X] is commutative. *)
+Global Instance commutative_hspace_pmap `{Funext} (X Y : pType)
+  `{IsCoherent X} `{!IsCohCommutative X}
+  : @Commutative (Y ->** X) _ (.*.).
+Proof.
+  intros f g.
+  snrapply path_pforall.
+  snrapply Build_pHomotopy.
+  - intros x.
+    nrapply commutativity.
+    exact _.
+  - pelim f g.
+    nrefine (iscohcommutative @ _).
+    symmetry.
+    apply concat_pV.
+Defined.
+
+(** If the H-space structure on [X] is coherently associative, then the H-space structure on [Y ->** X] is associative. *)
+Global Instance associative_hspace_pmap `{Funext} (X Y : pType)
+  `{IsCoherent X} `{!IsCohAssociative X}
+  : @Associative (Y ->** X) (.*.).
+Proof.
+  hnf.
+  intros f g h.
+  snrapply path_pforall.
+  snrapply Build_pHomotopy.
+  - intros x.
+    nrapply simple_associativity.
+    exact _.
+  - simpl.
+    pelim f g h.
+    simpl.
+    hott_simpl.
+    rewrite inv_pp.
+    simpl.
+    hott_simpl.
+    rewrite <- (ap_V (.* pt)).
+    apply associative_iscohassoc_coh.
+Defined.
+
+(** If the H-space structure on [X] is a coherent H-space, then the H-space structure on [Y ->** X] is a H-monoid. *)
+Global Instance ishmonoid_hspace_pmap `{Funext} (X Y : pType) `{IsCohHMonoid X}
+  : IsHMonoid (Y ->** X) := {}.
+
+(** If the H-space structure on [X] is a coherent H-group, then the H-space structure on [Y ->** X] is a H-group. *)
+Global Instance ishgroup_hspace_pmap `{Funext} (X Y : pType) `{IsCohHGroup X}
+  : IsHGroup (Y ->** X).
+Proof.
+  snrapply Build_IsHGroup.
+  1: exact _.
+  - intro f.
+    snrapply Build_pMap.
+    + exact (fun y => negate (f y)).
+    + nrefine (ap _ (point_eq f) @ _).
+      apply negate_coh.
+  - intro f.
+    snrapply path_pforall.
+    snrapply Build_pHomotopy.
+    + intro y.
+      cbn; apply left_inverse.
+    + pelim f.
+      simpl.
+      hott_simpl.
+      apply left_inverse_coh.
+  - intro f.
+    snrapply path_pforall.
+    snrapply Build_pHomotopy.
+    + intro y.
+      cbn; apply right_inverse.
+    + pelim f.
+      simpl.
+      hott_simpl.
+      apply right_inverse_coh.
+Defined.
+
+(** If the H-space structure on [X] is a coherent H-abelian group, then the H-space structure on [Y ->** X] is a H-AbGroup. *)
+Global Instance ishabgroup_hspace_pmap `{Funext} (X Y : pType) `{IsCohHAbGroup X}
+  : IsHAbGroup (Y ->** X) := {}.