`{Univalence} {A B C : AbGroup} (f : A $-> B) (g : A $-> C) `{IsEmbedding g} : IsEmbedding (ab_pushout_inl (f:=f) (g:=g)). Proof. apply isembedding_isinj_hset. intros c0 c1. refine (_ o (path_ab_pushout f g (grp_prod_inl c0) (grp_prod_inl c1))^-1). rapply Trunc_ind. cbn; intros [a p]. assert (z : a = mon_unit). - rapply (isinj_embedding g). refine (ap snd p @ _); cbn. exact (left_inverse mon_unit @ (grp_homo_unit g)^). - apply (grp_moveR_M1). refine (_ @ ap fst p); cbn; symmetry. refine (_ @ negate_mon_unit). refine (ap _ _). exact (ap f z @ grp_homo_unit f). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.