`{Univalence} {A B : AbGroup@{u}} : GroupIsomorphism A B <~> (A = B). Proof. refine (equiv_ap_inv issig_abgroup _ _ oE _). refine (equiv_path_sigma_hprop _ _ oE _). exact equiv_path_group. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.