{G H : Group} (X : G -> Type) (Y : H -> Type) (f : G $-> H) (preserves : forall g, X g -> Y (f g)) : forall g, subgroup_generated X g -> subgroup_generated Y (f g). Proof. intro g. apply Trunc_functor. intro p. induction p as [g i | | g h p1 IHp1 p2 IHp2]. - apply sgt_in, preserves, i. - rewrite grp_homo_unit. apply sgt_unit. - rewrite grp_homo_op, grp_homo_inv. by apply sgt_op. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.