Definition epis_Pushout {x y z: A} (E1 : Epi A x y) (E2 : Epi A x z) : Pushout E1 E2. Proof. set (coker1 := EpiToCokernel E1). set (coker2 := EpiToCokernel E2). set (BinCoprod := to_BinCoproducts A (to_Kernels A x y E1) (to_Kernels A x z E2)). set (ar := BinCoproductArrow BinCoprod (KernelArrow (to_Kernels A x y E1)) (KernelArrow (to_Kernels A x z E2))). set (coker := to_Cokernels A _ _ ar). use (make_Pushout E1 E2 coker (CokernelOut (to_Zero A) coker1 coker (CokernelArrow coker) (epis_Pushout_eq1 E1 E2 BinCoprod coker)) (CokernelOut (to_Zero A) coker2 coker (CokernelArrow coker) (epis_Pushout_eq2 E1 E2 BinCoprod coker)) (epis_Pushout_eq3 E1 E2 BinCoprod coker) (epis_Pushout_isPushout E1 E2 BinCoprod coker)). 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.opp_precat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. 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.Opp. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. isKernel (to_Zero A) (ZeroArrowFrom x) M (ArrowsFromZero A (to_Zero A) y (ZeroArrowFrom x · M) (ZeroArrow (to_Zero A) _ _)). make_Kernel (to_Zero A) (ZeroArrowFrom _) M _ (MonicKernelZero_isKernel M). - intros y0 Y. apply ArrowsFromZero.