x y : _ <~> @IsSemiGroup x y := ltac:(issig). Global Instance ishprop_issemigroup `{Funext} : forall x y, IsHProp (@IsSemiGroup x y). Proof. intros x y; apply istrunc_S; intros a b. rewrite <- (eisretr ( x y) a). rewrite <- (eisretr ( x y) b). set (a' := ( x y)^-1 a). set (b' := ( x y)^-1 b). clearbody a' b'; clear a b. srapply (contr_equiv _ (ap ( x y))). rewrite <- (eissect (equiv_sigma_prod0 _ _) a'). rewrite <- (eissect (equiv_sigma_prod0 _ _) b'). set (a := equiv_sigma_prod0 _ _ a'). set (b := equiv_sigma_prod0 _ _ b'). clearbody a b; clear a' b'. srapply (contr_equiv _ (ap (equiv_sigma_prod0 _ _)^-1)). srapply (contr_equiv _ (equiv_path_prod _ _)). srapply contr_prod. destruct a as [a' a], b as [b' b]. do 3 (nrefine (contr_equiv' _ (@equiv_path_forall H _ _ _ _)); nrefine (@contr_forall H _ _ _); intro). exact _. Defined.
Require Import Spaces.Nat.Core. Require Import Modalities.ReflectiveSubuniverse.