`{funext : Funext} (G H K : Group) : (GroupHomomorphism G K) * (GroupHomomorphism H K) <~> GroupHomomorphism (FreeProduct G H) K. Proof. refine (equiv_amalgamatedfreeproduct_rec _ _ _ _ _ K oE _^-1). refine (equiv_sigma_prod0 _ _ oE equiv_functor_sigma_id (fun _ => equiv_sigma_contr _)). intros f. rapply contr_forall. intros []; apply contr_inhab_prop. apply tr. 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.