{A B Y : AbGroup} (a : A $-> Y) (b : B $-> Y) : (ab_biprod_rec a b) $o ab_biprod_inr == b. Proof. intro y; simpl. rewrite (grp_homo_unit a). exact (left_identity (b y)). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.