{A A' B B' : AbGroup} (i : A $-> B) (i' : A' $-> B') `{IsEmbedding i} `{IsEmbedding i'} : IsEmbedding (functor_ab_biprod i i'). Proof. intros [b b']. apply hprop_allpath. intros [[a0 a0'] p] [[a1 a1'] p']; cbn in p, p'. rapply path_sigma_hprop; cbn. pose (q := (equiv_path_prod _ _)^-1 p); cbn in q. pose (q' := (equiv_path_prod _ _)^-1 p'); cbn in q'. destruct q as [q0 q1], q' as [q0' q1']. apply path_prod; rapply isinj_embedding; cbn. - exact (q0 @ q0'^). - exact (q1 @ q1'^). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.