Definition AddEquivUnitIso {A1 A2 : CategoryWithAdditiveStructure} (AE : AddEquiv A1 A2) (X : A1) : z_iso X (AddEquiv2 AE (AddEquiv1 AE X)). Proof. use make_z_iso. - exact (AddEquivUnit AE X). - exact (AddEquivUnitInvMor AE X). - exact (AddEquivUnitInvMor_is_inverse_in_precat AE X). Defined.
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.