{G : Group} (H : Subgroup G) : subgroup_group H $-> G. Proof. snrapply Build_GroupHomomorphism. 1: exact pr1. hnf; reflexivity. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.