proposition: Lemma equiv_path_biprod_corec `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X) : ((phi $o ab_biprod_inl == psi $o ab_biprod_inl) * (phi $o ab_biprod_inr == psi $o ab_biprod_inr)) <~> phi == psi.
proof: Proof. apply equiv_iff_hprop. - intros [h k]. intros [a b]. refine (ap phi (ab_biprod_decompose _ _) @ _ @ ap psi (ab_biprod_decompose _ _)^). refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^). exact (ap011 (+) (h a) (k b)). - intro h. exact (fun a => h _, fun b => h _). Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse