GroupHomomorphism K AmalgamatedFreeProduct. Proof. snrapply Build_GroupHomomorphism. { intro x. exact (amal_eta [inr x]). } intros x y. rewrite <- (app_nil [inr (x * y)]). rewrite <- (amal_mu_K nil nil x y). rewrite app_nil. reflexivity. Defined.
Require Import Basics Types. Require Import Cubical.DPath. Require Import Spaces.List.Core Spaces.List.Theory. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.Groups.Group. Require Import WildCat.