w x y z : _ <~> @IsGroup w x y z := ltac:(issig). Global Instance ishprop_isgroup `{Funext} w x y z : IsHProp (@IsGroup w x y z). Proof. apply istrunc_S. intros a b. rewrite <- (eisretr ( w x y z) a). rewrite <- (eisretr ( w x y z) b). set (a' := ( w x y z)^-1 a). set (b' := ( w x y z)^-1 b). clearbody a' b'; clear a b. srapply (contr_equiv _ (ap ( w x y z))). 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]; cbn. 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 _ _)). destruct a'' as [a a''], b'' as [b b'']; cbn. srapply contr_prod. all: srapply contr_paths_contr. all: srapply contr_inhabited_hprop. all: srapply istrunc_forall. Defined.
Require Import Spaces.Nat.Core. Require Import Modalities.ReflectiveSubuniverse.