Definition AbelianTocategoryWithAbgropsData : categoryWithAbgropsData AbelianToprecategoryWithBinops. Proof. unfold categoryWithAbgropsData. intros x y. split. - use make_isgrop. + split. * intros f g h. apply AbelianPreCat_homset_assoc. * use make_isunital. -- apply AbelianPreCat_homset_zero. -- split. ++ intros f. apply AbelianPreCat_homset_zero_left. ++ intros f. apply AbelianPreCat_homset_zero_right. + use tpair. * intros f. apply (AbelianPreCat_homset_inv f). * split. -- intros f. apply AbelianPreCat_homset_inv_left. -- intros f. apply AbelianPreCat_homset_inv_right. - intros f g. apply AbelianPreCat_homset_comm. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. + intros y H. apply ArrowsFromZero.