(X : Group) (h : GroupHomomorphism H X) (k : GroupHomomorphism K X) (p : h o f == k o g) : GroupHomomorphism AmalgamatedFreeProduct X. Proof. snrapply Build_GroupHomomorphism. 1: srapply (' X h k p). exact _. 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.