{G : Group} (X : G -> Type) : G -> Type := (** The subgroup should contain all elements of the original family.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.