proposition: Proposition ab_pushout_commsq {A B C : AbGroup} {f : A $-> B} {g : A $-> C} : (@ab_pushout_inl A B C f g) $o f == ab_pushout_inr $o g.
proof: Proof. intro a. apply qglue; cbn. apply tr. exists a. apply path_prod; simpl. - exact (right_identity _)^. - rewrite negate_mon_unit. exact (left_identity _)^. Defined.
imports: Basics Types Truncations.Core Modalities.ReflectiveSubuniverse WildCat.Core HSet Algebra.Groups.Image Algebra.Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.Biproduct