`{Univalence} {A B : AbGroup} : (A = B :> AbGroup) <~> (A = B :> Group) := equiv_path_group oE equiv_path_abgroup^-1. Global Instance isabgroup_subgroup (G : AbGroup) (H : Subgroup G) : IsAbGroup H. Proof. nrapply Build_IsAbGroup. 1: exact _. intros x y. apply path_sigma_hprop. cbn. apply commutativity. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.