`{Univalence} {G : Group} (X Y : G -> Type) (K : forall g, Trunc (-1) (X g) <-> Trunc (-1) (Y g)) : subgroup_generated X = subgroup_generated Y. Proof. rapply equiv_path_subgroup'. intro g; split. - apply path_subgroup_generated_helper, (fun x => fst (K x)). - apply path_subgroup_generated_helper, (fun x => snd (K x)). Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.