`{F : Funext} {G H : Group} : IsHSet (GroupIsomorphism G H). Proof. apply istrunc_S. intros f g; apply (istrunc_equiv_istrunc _ (equiv_path_groupisomorphism _ _)). Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.