Definition abgr_epi_cokernel_out_data_mult {A B C : abgr} (b1 b2 : B) (f : abgr_category⟦A, B⟧) (isE : isEpi f) (h : abgr_category⟦A, C⟧) (H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) : (∑ x : C, ∏ (hfib : hfiber (pr1 f) b1), pr1 h (pr1 hfib) = x) -> (∑ x : C, ∏ (hfib : hfiber (pr1 f) b2), pr1 h (pr1 hfib) = x) -> (∑ x : C, ∏ (hfib : hfiber (pr1 f) (b1 * b2)%multmonoid), pr1 h (pr1 hfib) = x). Proof. intros X X0. exact (tpair _ ((pr1 X) * (pr1 X0))%multmonoid (abgr_epi_CokernelOut_mult_eq b1 b2 f isE h H X X0)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. 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. 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.BinDirectSums. @ZeroArrowFrom abgr_category abgr_Zero A = abgrfunfromunit A.