Lemma AddEquivUnitMorComm {A1 A2 : CategoryWithAdditiveStructure} (AE : AddEquiv A1 A2) {x x' : ob A1} (f : x --> x') : f = (AddEquivUnitIso AE x) · (# (functor_composite (AddEquiv1 AE) (AddEquiv2 AE)) f) · (inv_from_z_iso (AddEquivUnitIso AE x')). Proof. use (post_comp_with_z_iso_is_inj (AddEquivUnitIso AE x')). use (pathscomp0 (AddEquivUnitComm AE _ _ f)). rewrite <- assoc. set (tmp := is_inverse_in_precat2 (AddEquivUnitIso AE x')). cbn in tmp. cbn. rewrite tmp. clear tmp. rewrite id_right. apply idpath. 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.