{A B : Group} (f g : A $-> B) : Group. Proof. rapply (AmalgamatedFreeProduct (FreeProduct A A) A B). 1,2: apply FreeProduct_rec. + exact grp_homo_id. + exact grp_homo_id. + exact f. + exact g. Defined.
Require Import Basics Types. Require Import WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Colimits.Coeq. Require Import Algebra.Groups.FreeProduct.