AmalgamatedFreeProduct_rec' (X : Group) (h : GroupHomomorphism H X) (k : GroupHomomorphism K X) (p : h o f == k o g) : AmalgamatedFreeProduct -> X. Proof. srapply amal_type_rec. { intro w. refine (fold_right _ _ w). { intros [l|r] x. + exact (h l * x). + exact (k r * x). } exact mon_unit. } { intros x y h1 h2; hnf. rewrite ?fold_right_app. f_ap. simpl. rewrite simple_associativity. f_ap. symmetry. exact (grp_homo_op h h1 h2). } { intros x y k1 k2; hnf. rewrite ?fold_right_app. f_ap. simpl. rewrite simple_associativity. f_ap. symmetry. exact (grp_homo_op k k1 k2). } { intros x y z; hnf. rewrite ?fold_right_app. f_ap; simpl; f_ap. } { intros x y; hnf. rewrite ?fold_right_app. f_ap. simpl. rewrite grp_homo_unit. rapply left_identity. } { intros x y; hnf. rewrite ?fold_right_app. f_ap. simpl. rewrite grp_homo_unit. rapply left_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.