equiv_path_subgroup' `{U : Univalence} {G : Group} (H K : Subgroup G) : (forall g:G, H g <-> K g) <~> (H = K). Proof. refine (equiv_path_subgroup _ _ oE _). apply equiv_functor_forall_id; intro g. exact equiv_path_iff_ishprop. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.