{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. intro a. apply qglue; cbn. apply tr. exists a. apply path_prod; simpl. - exact (right_identity _)^. - rewrite negate_mon_unit. exact (left_identity _)^. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.