`{F : Funext} {G H : Group} (f g : GroupIsomorphism G H) : f == g <~> f = g. Proof. refine ((equiv_ap (issig_GroupIsomorphism G H)^-1 _ _)^-1 oE _). refine (equiv_path_sigma_hprop _ _ oE _). apply equiv_path_grouphomomorphism. 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.