Definition ShortExact_from_ShortShortExact (SSE : ShortShortExact A) : ShortExact A. Proof. use make_ShortExact. - use make_ShortShortExact. + use make_ShortShortExactData. * use make_MorphismPair. -- exact (Abelian.Image (Mor1 SSE)). -- exact (Ob2 SSE). -- exact (Abelian.CoImage (Mor2 SSE)). -- exact (KernelArrow (Abelian.Image (Mor1 SSE))). -- exact (CokernelArrow (Abelian.CoImage (Mor2 SSE))). * exact (ShortExact_from_ShortShortExact_eq SSE). + exact (ShortExact_ShortShortExact_isKernel SSE). - exact (KernelArrowisMonic (to_Zero A) _). - exact (CokernelArrowisEpi (to_Zero A) _). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Opp. 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.Morphisms. 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.AbelianToAdditive. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.