(G : Group) : GroupHomomorphism G grp_trivial. Proof. snrapply Build_GroupHomomorphism. 1: exact (fun _ => tt). intros ??; symmetry; exact (grp_unit_l _). Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.