`{Funext} (X : Group) : {h : GroupHomomorphism H X & {k : GroupHomomorphism K X & h o f == k o g }} <~> GroupHomomorphism AmalgamatedFreeProduct X. Proof. snrapply equiv_adjointify. 1: intros [h [k p]]; exact (AmalgamatedFreeProduct_rec X h k p). { intros r. exists (grp_homo_compose r amal_inl). exists (grp_homo_compose r amal_inr). intro x. apply (ap r). simpl. rewrite <- (app_nil [inl (f x)]). rewrite <- (app_nil [inr (g x)]). apply (amal_tau nil nil x). } { intros r. apply equiv_path_grouphomomorphism. srapply amal_type_ind_hprop. intro x. induction x as [|a x]. 1: symmetry; apply (grp_homo_unit r). simpl in *. rewrite IHx. destruct a; symmetry; rapply (grp_homo_op r (amal_eta [_]) (amal_eta x)). } intro hkp. simpl. rapply (equiv_ap' (equiv_sigma_prod (fun hk : GroupHomomorphism H X * GroupHomomorphism K X => fst hk o f == snd hk o g)) _ _)^-1%equiv. rapply path_sigma_hprop. destruct hkp as [h [k p]]. apply path_prod; cbn; apply equiv_path_grouphomomorphism; intro; simpl; rapply right_identity. 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.