(G H K : Group) (f : GroupHomomorphism G K) (g : GroupHomomorphism H K) : GroupHomomorphism (FreeProduct G H) K. Proof. snrapply (AmalgamatedFreeProduct_rec _ _ _ _ _ _ f g). intros []. refine (grp_homo_unit _ @ (grp_homo_unit _)^). 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.