{A B C : AbGroup} {f g : ab_biprod A B $-> C} (Hinl : f $o ab_biprod_inl $== g $o ab_biprod_inl) (Hinr : f $o ab_biprod_inr $== g $o ab_biprod_inr) : f $== g. Proof. rapply ab_biprod_ind. - exact Hinl. - exact Hinr. - intros x y p q. lhs nrapply grp_homo_op. rhs nrapply grp_homo_op. f_ap. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.