proposition: Proposition ab_biprod_rec_beta' {A B Y : AbGroup} (u : ab_biprod A B $-> Y) : ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) == u.
proof: Proof. intros [a b]; simpl. refine ((grp_homo_op u _ _)^ @ ap u _). apply path_prod. - exact (right_identity a). - exact (left_identity b). Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse