{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. intros [a b]; simpl. refine ((grp_homo_op u _ _)^ @ ap u _). apply path_prod. - exact (right_identity a). - exact (left_identity b). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.