Lemma AddEquiv1Inj {A1 A2 : CategoryWithAdditiveStructure} (AE : AddEquiv A1 A2) {x y : A1} (f g : x --> y) (H : # (AddEquiv1 AE) f = # (AddEquiv1 AE) g) : f = g. Proof. apply (maponpaths (# (AddEquiv2 AE))) in H. use (post_comp_with_z_iso_is_inj (AddEquivUnitIso AE y)). use (pathscomp0 (AddEquivUnitComm AE _ _ f)). use (pathscomp0 _ (! (AddEquivUnitComm AE _ _ g))). exact (maponpaths (λ gg : _, (AddEquivUnit AE) x · gg) H). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. exists (ZeroArrowFrom (F (to_Zero A))). apply ArrowsFromZero. assert (e2 : # F (ZeroArrowFrom a2) = @ZeroArrowFrom B Z (F a2)). apply (ArrowsFromZero B Z). use (FromBinDirectSumsEq B BDS); cbn.