(G : Group) := { subgroup_pred : G -> Type ; subgroup_issubgroup : IsSubgroup subgroup_pred ; }.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.