Require Export UniMath.Foundations.All.
Require Export UniMath.CategoryTheory.Monics.
Require Export UniMath.CategoryTheory.Epis.
Require Export UniMath.CategoryTheory.limits.zero.
Require Export UniMath.CategoryTheory.limits.kernels.
Require Export UniMath.CategoryTheory.limits.cokernels.
Require Export UniMath.CategoryTheory.limits.binproducts.
Require Export UniMath.CategoryTheory.limits.bincoproducts.
Require Export UniMath.CategoryTheory.limits.pullbacks.
Require Export UniMath.CategoryTheory.limits.pushouts.
Require Export UniMath.CategoryTheory.limits.BinDirectSums.
Require Export UniMath.CategoryTheory.limits.Opp.
Require Export UniMath.CategoryTheory.CategoriesWithBinOps.
Require Export UniMath.CategoryTheory.Categories.
Require Export UniMath.CategoryTheory.opp_precat.
Require Export UniMath.CategoryTheory.PrecategoriesWithAbgrops.
Require Export UniMath.CategoryTheory.PreAdditive.
Require Export UniMath.CategoryTheory.Morphisms.
Require Export UniMath.CategoryTheory.Additive.
Require Export UniMath.CategoryTheory.functor_categories.
Require Export UniMath.CategoryTheory.Subcategory.Full.
Require Export UniMath.MoreFoundations.Notations.
Require Export UniMath.MoreFoundations.PartA.
Require Export UniMath.MoreFoundations.Propositions.
Require Export UniMath.Algebra.BinaryOperations.
Require Export UniMath.Algebra.Monoids_and_Groups.

Local Arguments isZero {_} _.
Local Arguments BinDirectSumOb {_ _ _}.
Local Arguments to_binop {_ _ _}.
Local Arguments grinv {_}.
Local Arguments BinDirectSum {_}.
Local Arguments to_Pr1 {_ _ _} _.
Local Arguments to_Pr2 {_ _ _} _.
Local Arguments to_In1 {_ _ _} _.
Local Arguments to_In2 {_ _ _} _.
Local Arguments to_BinOpId {_ _ _ _ _ _ _ _}.
Local Arguments to_IdIn1 {_ _ _ _ _ _ _ _}.
Local Arguments to_IdIn2 {_ _ _ _ _ _ _ _}.
Local Arguments to_Unel1 {_ _ _ _ _ _ _ _}.
Local Arguments to_Unel2 {_ _ _ _ _ _ _ _}.
Local Arguments MorphismPair : clear implicits.
Local Arguments morphism_from_iso {_ _ _}.
Local Arguments ToBinDirectSum {_ _ _} _ {_}.
Local Arguments isBinDirectSum {_ _ _ _}.

Local Open Scope logic.
Local Open Scope cat.

Local Definition hom (C:precategory_data) : ob C → ob C → UU := λ c c', precategory_morphisms c c'.
Local Definition Hom (C : category) : ob C → ob C → hSet := λ c c', hSetpair _ (homset_property C c c').
Local Definition Hom_add (C : PreAdditive) : ob C → ob C → abgr := λ c c', (@to_abgr C c c').


Section InvestigateNotations.
  Context (M : PreAdditive) (x y z:M) (f g : hom M x y) (h k : Hom_add M y z).
  Local Open Scope abgrcat.
  Goal empty.
    set (Q := h+k).
    set (r := -g).
    set (t := f-g).
    set (p := f·h + (h∘f) · 1).
    set (o := (h + h) · 1 = h).
    set (s := f+g).
    set (u := f·1).
    set (v := f·0·h).
  Abort.
End InvestigateNotations.

Section Categories.
  Definition isPushout' {M:category} {a b c d : M} (f : a --> b) (g : a --> c)
             (in1 : b --> d) (in2 : c --> d) : hProp.
  Proof.
    ∃ (∑ (H : f · in1 = g · in2), isPushout f g in1 in2 H).
    abstract (
        apply isaproptotal2 ;
        [ intros H; apply isaprop_isPushout
        | intros H H' po po'; apply homset_property ]) using _P_.
  Defined.
  Definition isPullback' {M:category} {a b c d : M} (f : b --> a) (g : c --> a)
             (p1 : d --> b) (p2 : d --> c) : hProp.
  Proof.
    ∃ (∑ (H : p1 · f = p2· g), isPullback f g p1 p2 H).
    exact (_P_ (oppositeCategory M) a b c d f g p1 p2).
  Defined.
  Lemma isPullback'_up_to_z_iso {M:category} {a b c d d' : M}
        (f : b --> a) (g : c --> a) (p1 : d --> b) (p2 : d --> c)
        (i : z_iso d' d) :
    isPullback' f g p1 p2 → isPullback' f g (i·p1) (i·p2).
  Proof.
    intros [e pb]. use tpair.
    - abstract (rewrite 2 assoc'; apply maponpaths; exact e) using _P_.
    - cbn beta. intros T r s eq.
      assert (Q := pb T r s eq).
      use (iscontrweqf _ Q); clear Q.
      use weqtotal2.
      { apply z_iso_comp_left_weq. exact (z_iso_inv i). }
      { intros h. cbn beta. apply weqiff.
        { cbn.
          rewrite 2 (assoc' h). rewrite 2 (assoc _ i).
          rewrite z_iso_after_z_iso_inv. rewrite 2 id_left.
          apply isrefl_logeq. }
        { apply isapropdirprod; apply homset_property. }
        { apply isapropdirprod; apply homset_property. }
        }
  Defined.
  Lemma isPushout'_up_to_z_iso {M:category} {a b c d d' : M}
        (f : a --> b) (g : a --> c) (in1 : b --> d) (in2 : c --> d)
        (i : z_iso d d') :
    isPushout' f g in1 in2 → isPushout' f g (i∘in1) (i∘in2).
  Proof.
    exact (isPullback'_up_to_z_iso (M:=oppositeCategory M) f g in1 in2 (opp_z_iso i)).
  Qed.
  Lemma Pushout_to_isPushout' {M:category} {a b c : M} (f : a --> b) (g : a --> c)
        (po : Pushout f g) :
    isPushout' f g (PushoutIn1 po) (PushoutIn2 po).
  Proof.
    use tpair.
    - apply PushoutSqrCommutes.
    - cbn beta. apply isPushout_Pushout.
  Qed.
  Lemma Pullback_to_isPullback' {M:category} {a b c : M} (f : b --> a) (g : c --> a)
        (pb : Pullback f g) :
    isPullback' f g (PullbackPr1 pb) (PullbackPr2 pb).
  Proof.
    use tpair.
    - apply PullbackSqrCommutes.
    - cbn beta. apply isPullback_Pullback.
  Qed.
End Categories.

Section MorphismPairs.
  Goal ∏ (M : precategory) (P Q : MorphismPair M) (f:MorphismPairIsomorphism P Q),
       InverseMorphismPairIsomorphism (InverseMorphismPairIsomorphism f) = f.
  Proof.
    Fail reflexivity.
  Abort.
End MorphismPairs.

Section Pullbacks.   Definition IsoArrowTo {M : precategory} {A A' B:M} (g : A --> B) (g' : A' --> B) := ∑ i : z_iso A A', i · g' = g .
  Coercion IsoArrowTo_pr1 {M : precategory} {A A' B:M} (g : A --> B) (g' : A' --> B) : IsoArrowTo g g' → z_iso A A' := pr1.
  Definition IsoArrowFrom {M : precategory} {A B B':M} (g : A --> B) (g' : A --> B') := ∑ i : z_iso B B', g · i = g'.
  Coercion IsoArrowFrom_pr1 {M : precategory} {A B B':M} (g : A --> B) (g' : A --> B') : IsoArrowFrom g g' → z_iso B B' := pr1.
  Definition IsoArrow {M : precategory} {A A' B B':M} (g : A --> B) (g' : A' --> B') := ∑ (i : z_iso A A') (j : z_iso B B'), i · g' = g · j.
  Definition pullbackiso1 {M : precategory} {A B C:M} {f : A --> C} {g : B --> C}
        (pb : Pullback f g) (pb' : Pullback f g)
    : IsoArrowTo (PullbackPr1 pb) (PullbackPr1 pb')
    := pr1 (pullbackiso pb pb'),,pr12 (pullbackiso pb pb').
  Definition pullbackiso2 {M : precategory} {A B C:M} {f : A --> C} {g : B --> C}
        (pb : Pullback f g) (pb' : Pullback f g)
    : IsoArrowTo (PullbackPr2 pb) (PullbackPr2 pb')
    := pr1 (pullbackiso pb pb'),,pr22 (pullbackiso pb pb').
  Section OppositeIsoArrows.
    Definition opposite_IsoArrowTo {M:precategory} {A A' B:M} {g : A --> B} {g' : A' --> B} :
      IsoArrowTo g g' → IsoArrowFrom (M:=M^op) g' g.
    Proof.
      intros i.
      Fail exact i.
      use tpair.
      - exact (opp_z_iso (pr1 i)).
      - cbn. exact (pr2 i).
    Defined.
    Definition opposite_IsoArrowFrom {M:precategory} {A B B':M} {g : A --> B} {g' : A --> B'} :
      IsoArrowFrom g g' → IsoArrowTo (M:=M^op) g' g.
    Proof.
      intros i. use tpair.
      - exact (opp_z_iso (pr1 i)).
      - cbn. exact (pr2 i).
    Defined.
    Definition opposite_IsoArrow {M:precategory} {A A' B B':M} (g : A --> B) (g' : A' --> B') :
      IsoArrow g g' → IsoArrow (M:=M^op) (opp_mor g') (opp_mor g).
    Proof.
      intros i.
      ∃ (opp_z_iso (pr12 i)).
      ∃ (opp_z_iso (pr1 i)).
      exact (! pr22 i).
    Defined.
  End OppositeIsoArrows.
  Lemma IsoArrowTo_isaprop (M : category) {A A' B:M} (g : A --> B) (g' : A' --> B) :
    isMonic g' → isaprop (IsoArrowTo g g').
  Proof.
    intros i. apply invproofirrelevance; intros k k'. apply subtypeEquality'.
    - induction k as [[k K] e], k' as [[k' K'] e']; cbn; cbn in e, e'.
      induction (i A k k' (e @ !e')). apply maponpaths. apply isaprop_is_z_isomorphism.
      apply homset_property.
    - apply homset_property.
  Qed.
  Lemma IsoArrowFrom_isaprop (M : category) {A B B':M} (g : A --> B) (g' : A --> B') :
     isEpi g → isaprop (IsoArrowFrom g g').
  Proof.
    intros i. apply invproofirrelevance; intros k k'. apply subtypeEquality.
    { intros j. apply homset_property. }
    induction k as [[k K] e], k' as [[k' K'] e']; cbn; cbn in e, e'.
    apply subtypeEquality; cbn.
    { intros f. apply isaprop_is_z_isomorphism. apply homset_property. }
    use i. exact (e @ !e').
  Qed.
End Pullbacks.

Local Open Scope abgrcat.

Local Notation "0" := (unel (grtomonoid (abgrtogr _))) : abgrcat.
Local Notation "0" := (unel (grtomonoid (abgrtogr (to_abgr _ _)))) : abgrcat.
Local Notation "f + g" := (@op (pr1monoid (grtomonoid (abgrtogr _))) f g) : abgrcat.
Local Notation "f + g" := (@op (pr1monoid (grtomonoid (abgrtogr (to_abgr _ _)))) f g) : abgrcat.
Local Notation " - g" := (@grinv (abgrtogr _) g) : abgrcat.
Local Notation " - g" := (@grinv (abgrtogr (to_abgr _ _)) g) : abgrcat.
Local Notation "f - g" := (@op (pr1monoid (grtomonoid (abgrtogr _))) f (@grinv (abgrtogr (to_abgr _ _)) g)) : abgrcat.
Local Notation "f - g" := (@op (pr1monoid (grtomonoid (abgrtogr (to_abgr _ _)))) f (@grinv (abgrtogr (to_abgr _ _)) g)) : abgrcat.

Section PreAdditive.

  Lemma ThroughZeroIsZero {M:PreAdditive} (a b:M) (Z : Zero M) (f : a --> Z) (g : Z --> b) : f · g = 0.
  Proof.
    intermediate_path ((0:a-->Z) · g).
    - apply (maponpaths (postcomp_with g)). apply ArrowsToZero.
    - apply to_postmor_unel'.
  Qed.
  Definition elem21 {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:A-->B) : AB-->AB := 1 + π₁·f·ι₂.
  Section Foo.     Definition elem21_isiso {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:A-->B) : is_z_isomorphism (elem21 AB f).
    Proof.
      ∃ (1 - π₁·f·ι₂).
      unfold elem21. split.
      - rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
        rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite rightMinus.
        rewrite <- assocax. rewrite grlinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc π₁ f ι₂).
        rewrite (assoc ι₂). rewrite DirectSumIn2Pr1. rewrite zeroLeft. rewrite zeroRight.
        rewrite grinvunel. reflexivity.
      - rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
        rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite leftMinus.
        rewrite <- assocax. rewrite grrinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc π₁ f ι₂).
        rewrite (assoc ι₂). rewrite DirectSumIn2Pr1. rewrite zeroLeft. rewrite zeroRight.
        rewrite grinvunel. reflexivity.
    Defined.
  End Foo.
  Definition elem12 {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:B-->A) : AB-->AB := 1 + π₂·f·ι₁.
  Definition elem12_isiso {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:B-->A) : is_z_isomorphism (elem12 AB f).
  Proof.
    ∃ (1 - π₂·f·ι₁). unfold elem12. split.
    - rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
      rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite rightMinus.
      rewrite <- assocax. rewrite grlinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc _ f _).
      rewrite 2 (assoc ι₁). rewrite DirectSumIn1Pr2. rewrite zeroLeft. rewrite zeroLeft.
      rewrite 2 zeroRight.
      use grinvunel.
    - rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
      rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite leftMinus.
      rewrite <- assocax. rewrite grrinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc _ f _).
      rewrite (assoc ι₁). rewrite (assoc ι₁). rewrite DirectSumIn1Pr2. rewrite 2 zeroLeft.
      rewrite 2 zeroRight. use grinvunel.
  Defined.
  Definition isKernel' {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) : hProp :=
    f · g = 0 ∧ ∀ (w : M) (h : w --> y), h · g = 0 ⇒ ∃! φ : w --> x, φ · f = h.
  Definition hasKernel {M:PreAdditive} {y z : M} (g : y --> z) : hProp :=
    ∃ x (f:x-->y), isKernel' f g.
  Lemma isKernel_iff {M:PreAdditive} {x y z : M} (Z:Zero M) (f : x --> y) (g : y --> z) :
    isKernel' f g ↔ ∑ e : f · g = ZeroArrow Z x z, isKernel Z f g e.
  Proof.
    split.
    { intros [e' ik].
      use tpair.
      { refine (e' @ _). apply PreAdditive_unel_zero. }
      intros T h e.
      exact (ik T h (e @ ! PreAdditive_unel_zero _ _ _ _)). }
    { intros [e ik]. use tpair.
      { refine (e @ ! _). apply PreAdditive_unel_zero. }
      cbn beta. intros T h e'.
      exact (ik T h (e' @ PreAdditive_unel_zero _ _ _ _)). }
  Qed.
  Definition isKernel'_to_Kernel {M:PreAdditive} (Z:Zero M) {x y z : M} (f : x --> y) (g : y --> z) :
    isKernel' f g → Kernel Z g.
  Proof.
    intros co. ∃ (x,,f). now apply isKernel_iff.
  Defined.
  Definition isCokernel' {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) : hProp :=
    f · g = 0 ∧ ∀ (w : M) (h : y --> w), f · h = 0 ⇒ ∃! φ : z --> w, g · φ = h.
  Definition hasCokernel {M:PreAdditive} {x y : M} (f : x --> y) : hProp :=
    ∃ z (g:y-->z), isCokernel' f g.
  Lemma isCokernel_iff {M:PreAdditive} {x y z : M} (Z:Zero M) (f : x <-- y) (g : y <-- z) :
    isCokernel' g f ↔ ∑ e : f ∘ g = ZeroArrow Z z x, isCokernel Z g f e.
  Proof.
    split.
    { intros [e' ik].
      use tpair.
      { refine (e' @ _). apply PreAdditive_unel_zero. }
      intros T h e.
      exact (ik T h (e @ ! PreAdditive_unel_zero _ _ _ _)). }
    { intros [e ik]. use tpair.
      { refine (e @ ! _). apply PreAdditive_unel_zero. }
      cbn beta. intros T h e'.
      exact (ik T h (e' @ PreAdditive_unel_zero _ _ _ _)). }
  Qed.
  Definition isCokernel'_to_Cokernel {M:PreAdditive} (Z:Zero M) {x y z : M} (f : x --> y) (g : y --> z) :
    isCokernel' f g → Cokernel Z f.
  Proof.
    intros co. ∃ (z,,g). now apply isCokernel_iff.
  Defined.
  Section Tmp.
    Lemma PushoutCokernel {M:PreAdditive} {A B C D E:M} (i:A-->B) (p:B-->C)
          (j:B-->D) (p':D-->E) (j':C-->E) :
      isCokernel' i p → isPushout' (M:=M) j p p' j' → isCokernel' (i·j) p'.
    Proof.
      intros [b co] [e po].
      split.
      - rewrite assoc'.
        Fail rewrite e.
        unfold categoryWithAbgrops_category, category_to_precategory, pr1 in e.
        rewrite e.
        rewrite assoc. rewrite b. apply zeroLeft.
      - intros T h v. rewrite assoc' in v.
        assert (Q := co T (j·h) v); cbn in Q. generalize Q; clear Q.
        apply iscontrweqb. use weqpair.
        + intros [k w]; ∃ (j'·k); abstract (rewrite assoc; unfold categoryWithAbgrops_category, category_to_precategory, pr1 in e; rewrite <- e; rewrite assoc';
          rewrite w; reflexivity) using _L_.
        + cbn beta. intros [l w]; unfold hfiber. assert (PO := po T h l (!w)); clear po.
          generalize PO; clear PO. apply iscontrweqb.
          refine (weqcomp (weqtotal2asstor _ _) _). apply weqfibtototal; intros m. cbn.
          apply weqiff.
          { split.
            - intros [x y]. split.
              + exact x.
              + exact (maponpaths pr1 y).
            - intros [x y]. ∃ x. induction y. apply maponpaths, to_has_homsets.
            }
          { apply isofhleveltotal2.
              - apply to_has_homsets.
              - intros u. refine ((_:isofhlevel 2 _) _ _). apply isofhleveltotal2.
                + apply to_has_homsets.
                + intros n. apply hlevelntosn. apply to_has_homsets. }
          { apply isapropdirprod; apply to_has_homsets. }
    Qed.
  End Tmp.
  Lemma PullbackKernel {M:PreAdditive} {A B C D E:M} (i:A<--B) (p:B<--C)
        (j:B<--D) (p':D<--E) (j':C<--E) :
    isKernel' p i → isPullback' (M:=M) j p p' j' → isKernel' p' (i∘j).
  Proof.
    exact (@PushoutCokernel (oppositePreAdditive M) A B C D E i p j p' j').
  Defined.
  Lemma KernelIsMonic {M:PreAdditive} {x y z:M} (f : x --> y) (g : y --> z) : isKernel' f g → isMonic f.
  Proof.
    intros [t i] w p q e.
    set (T := ∑ r : w --> x, r · f = q · f). assert (ic : isProofIrrelevant T).
    { apply proofirrelevance, isapropifcontr.
      use i. rewrite assoc'. rewrite t. apply zeroRight. }
    set (t1 := (p,,e) : T). set (t2 := (q,,idpath _) : T).
    assert (Q := ic t1 t2). exact (maponpaths pr1 Q).
  Qed.
  Lemma CokernelIsEpi {M:PreAdditive} {x y z:M} (f : x --> y) (g : y --> z) : isCokernel' f g → isEpi g.
  Proof.
    exact (KernelIsMonic (M:=oppositePreAdditive M) g f).
  Qed.
  Definition makeMonicKernel {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) :
    isMonic f → f · g = 0 →
    (∏ (w : M) (h : w --> y), h · g = 0 → ∑ φ : w --> x, φ · f = h) →
    isKernel' f g.
  Proof.
    intros im eq ex. ∃ eq. intros w h e.
    apply iscontraprop1.
    - apply invproofirrelevance; intros [r R] [s S].
      apply subtypeEquality_prop; simpl. apply im. exact (R@!S).
    - apply ex. exact e.
  Qed.
  Definition makeEpiCokernel {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) :
    isEpi g → f · g = 0 →
    (∏ (w : M) (h : y --> w), f · h = 0 → ∑ φ : z --> w, g · φ = h) →
    isCokernel' f g.
  Proof.
    exact (makeMonicKernel (M:=oppositePreAdditive M) g f).
  Qed.
  Lemma IsoWithKernel {M:PreAdditive} {x y z z':M} (f : x --> y) (g : y --> z) (h : z --> z') :
    isKernel' f g → is_z_isomorphism h → isKernel' f (g·h).
  Proof.
    intros i j.
    apply makeMonicKernel.
    - exact (KernelIsMonic _ _ i).
    - exact (assoc _ _ _ @ maponpaths (postcomp_with _) (pr1 i) @ zeroLeft h).
    - intros w k e. apply (pr2 i).
      refine (post_comp_with_iso_is_inj _ _ _ h (is_iso_from_is_z_iso h j) _ _ _ _).
      refine (! assoc _ _ _ @ e @ ! zeroLeft _).
  Qed.
  Lemma IsoWithCokernel {M:PreAdditive} {x x' y z:M} (f : x --> y) (g : y --> z) (h : x' --> x) :
    isCokernel' f g → is_z_isomorphism h → isCokernel' (h·f) g.
  Proof.
    exact (λ c i, IsoWithKernel (M:=oppositePreAdditive M) g f h c (opp_is_z_isomorphism h i)).
  Qed.
  Lemma KernelOfZeroMapIsIso {M:PreAdditive} {x y z:M} (g : x --> y) : isKernel' g (0 : y --> z) → is_z_isomorphism g.
  Proof.
    intros [_ ke]. use (is_z_iso_from_is_iso' M). intros T h. exact (ke _ _ (zeroRight _)).
  Defined.
  Lemma CokernelOfZeroMapIsIso {M:PreAdditive} {x y z:M} (g : y --> z) : isCokernel' (0 : x --> y) g → is_z_isomorphism g.
  Proof.
    intros [_ co]. use is_z_iso_from_is_iso. intros T h. exact (co _ _ (zeroLeft _)).
  Defined.
  Lemma KernelUniqueness {M:PreAdditive} {x x' y z : M} {f : x --> y} {f' : x' --> y} {g : y --> z} :
    isKernel' f g → isKernel' f' g → iscontr (IsoArrowTo f f').
  Proof.
    intros i j. apply iscontraprop1.
    - exact (IsoArrowTo_isaprop M f f' (KernelIsMonic f' g j)).
    - induction (iscontrpr1 (pr2 j _ f (pr1 i))) as [p P].
      induction (iscontrpr1 (pr2 i _ f' (pr1 j))) as [q Q].
      use tpair.
      + ∃ p. ∃ q. split.
        × apply (KernelIsMonic _ _ i). rewrite assoc'. rewrite Q. rewrite P. rewrite id_left. reflexivity.
        × apply (KernelIsMonic _ _ j). rewrite assoc'. rewrite P. rewrite Q. rewrite id_left. reflexivity.
      + cbn. exact P.
  Defined.
  Lemma CokernelUniqueness {M:PreAdditive} {x y z z' : M} {f : x --> y} {g : y --> z} {g' : y --> z'} :
    isCokernel' f g → isCokernel' f g' → iscontr (IsoArrowFrom g g').
  Proof.
    intros i j.
    apply iscontraprop1.
    - exact (IsoArrowFrom_isaprop M g g' (CokernelIsEpi f g i)).
    - induction (iscontrpr1 (pr2 j _ g (pr1 i))) as [p P].
      induction (iscontrpr1 (pr2 i _ g' (pr1 j))) as [q Q].
      use tpair.
      + ∃ q. ∃ p. split.
        × apply (CokernelIsEpi _ _ i). rewrite assoc. rewrite Q. rewrite P. rewrite id_right. reflexivity.
        × apply (CokernelIsEpi _ _ j). rewrite assoc. rewrite P. rewrite Q. rewrite id_right. reflexivity.
      + cbn. exact Q.
  Defined.
  Lemma DirectSumToPullback {M:PreAdditive} {A B:M} (S : BinDirectSum A B) (Z : Zero M) :
    Pullback (0 : A --> Z) (0 : B --> Z).
  Proof.
    use tpair.
    - ∃ S. exact (to_Pr1 S,, to_Pr2 S).
    - cbn. use tpair.
      + apply ArrowsToZero.
      + cbn. intros T f g e. exact (to_isBinProduct M S T f g).
  Defined.
  Lemma DirectSumToPushout {M:PreAdditive} {A B:M} (S : BinDirectSum A B) (Z : Zero M) :
    Pushout (0 : Z --> A) (0 : Z --> B).
  Proof.
    use tpair.
    - ∃ S. exact (to_In1 S,, to_In2 S).
    - cbn. use tpair.
      + apply ArrowsFromZero.
      + cbn. intros T f g e. exact (to_isBinCoproduct M S T f g).
  Defined.
  Definition directSumMap {M:PreAdditive} {a b c d:M} (ac : BinDirectSum a c) (bd : BinDirectSum b d) (f : a --> b) (g : c --> d) : ac --> bd
    := BinDirectSumIndAr M f g _ _.
  Lemma directSumMapEqPr1 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
    directSumMap ac bd f g · π₁ = π₁ · f.
  Proof.
    apply BinDirectSumPr1Commutes.
  Qed.
  Lemma directSumMapEqPr2 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
    directSumMap ac bd f g · π₂ = π₂ · g.
  Proof.
    apply BinDirectSumPr2Commutes.
  Qed.
  Lemma directSumMapEqIn1 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
    ι₁ · directSumMap ac bd f g = f · ι₁.
  Proof.
    unfold directSumMap. rewrite BinDirectSumIndArEq. apply BinDirectSumIn1Commutes.
  Qed.
  Lemma directSumMapEqIn2 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
    ι₂ · directSumMap ac bd f g = g · ι₂.
  Proof.
    unfold directSumMap. rewrite BinDirectSumIndArEq. apply BinDirectSumIn2Commutes.
  Qed.
  Definition to_BinOpId' {M:PreAdditive} {a b co : M} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
             (B : isBinDirectSum i1 i2 p1 p2) :
    p1 · i1 + p2 · i2 = identity co := to_BinOpId B.
  Definition to_BinOpId'' {M:PreAdditive} {a b : M} (ab : BinDirectSum a b)
             : (to_Pr1 ab · to_In1 ab) + (to_Pr2 ab · to_In2 ab) = 1
    := to_BinOpId ab.
  Definition ismonoidfun_prop {G H:abgr} (f:G→H) : hProp := hProppair (ismonoidfun f) (isapropismonoidfun f).
  Definition PreAdditive_functor (M N:PreAdditive) :=
    ∑ F : M ⟶ N, ∀ A B:M, ismonoidfun_prop (@functor_on_morphisms M N F A B : A --> B → F A --> F B).
  Coercion PreAdditive_functor_to_functor {M N:PreAdditive} : PreAdditive_functor M N → functor M N := pr1.
  Definition functor_on_morphisms_add {C C' : PreAdditive} (F : PreAdditive_functor C C') { a b : C}
    : monoidfun (a --> b) (F a --> F b)
    := monoidfunconstr (pr2 F a b).
  Local Notation "# F" := (functor_on_morphisms_add F) : abgrcat.
  Lemma add_functor_comp {M N:PreAdditive} (F : PreAdditive_functor M N) {A B C:M} (f:A --> B) (g:B --> C) :
    # F (f · g) = # F f · # F g.
  Proof.
    exact (functor_comp F f g).
  Qed.
  Lemma add_functor_add {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} (f g:A --> B) :
    # F (f+g) = # F f + # F g.
  Proof.
    exact (ismonoidfunisbinopfun (pr2 F A B) f g).
  Qed.
  Lemma add_functor_zero {M N:PreAdditive} (F : PreAdditive_functor M N) (A B:M) :
    functor_on_morphisms_add (a:=A) (b:=B) F 0 = 0.
  Proof.
    exact (ismonoidfununel (pr2 F A B)).
  Qed.
  Lemma add_functor_sub {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} (g:A --> B) :
    # F (-g) = - # F g.
  Proof.
    exact (grinvandmonoidfun _ _ (pr2 F A B) g).
  Qed.
  Lemma zeroCriterion {M:PreAdditive} {Z:M} : identity Z = 0 ↔ isZero Z.
  Proof.
    split.
    { intros e. split.
      - intros T. ∃ 0. intros h. refine (! id_left h @ _). induction (!e); clear e. apply zeroLeft.
      - intros T. ∃ 0. intros h. refine (! id_right h @ _). induction (!e); clear e. apply zeroRight. }
    { intros i. apply (isapropifcontr (pr1 i Z)). }
  Qed.
  Lemma applyFunctorToIsZero {M N:PreAdditive} (F : PreAdditive_functor M N) (Z : M) :
    isZero Z → isZero (F Z).
  Proof.
    exact (λ i, pr1 zeroCriterion (! functor_id F Z @ maponpaths (#F) (pr2 zeroCriterion i) @ add_functor_zero F Z Z)).
  Qed.
  Definition applyFunctorToZero {M N:PreAdditive} (F : PreAdditive_functor M N) : Zero M → Zero N.
  Proof.
    intros Z. exact (F Z,, applyFunctorToIsZero F Z (pr2 Z)).
  Defined.
  Definition applyFunctorToIsBinDirectSum {M N:PreAdditive} (F : PreAdditive_functor M N)
             (A B S : M) (i1 : A --> S) (i2 : B --> S) (p1 : S --> A) (p2 : S --> B) :
    isBinDirectSum i1 i2 p1 p2 → isBinDirectSum (# F i1) (# F i2) (# F p1) (# F p2).
  Proof.
    intros ds.
    repeat split.
    - rewrite <- add_functor_comp. rewrite (to_IdIn1 ds). apply functor_id.
    - rewrite <- add_functor_comp. rewrite (to_IdIn2 ds). apply functor_id.
    - rewrite <- add_functor_comp. rewrite (to_Unel1 ds); unfold to_unel. use ismonoidfununel. use (pr2 F).
    - rewrite <- add_functor_comp. rewrite (to_Unel2 ds); unfold to_unel. use ismonoidfununel. use (pr2 F).
    - rewrite <- 2 add_functor_comp. rewrite <- add_functor_add. rewrite (to_BinOpId' ds). apply functor_id.
  Qed.
  Definition applyFunctorToBinDirectSum {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} :
    BinDirectSum A B → BinDirectSum (F A) (F B)
    := λ S, mk_BinDirectSum _ _ _ _ _ _ _ _ (applyFunctorToIsBinDirectSum F A B S ι₁ ι₂ π₁ π₂ (pr2 S)).
  Definition induced_PreAdditive_incl (M : PreAdditive) {X:Type} (j : X → ob M) :
    PreAdditive_functor (induced_PreAdditive M j) M.
  Proof.
    ∃ (induced_precategory_incl j). intros A B. split.
    + intros f g. reflexivity.
    + reflexivity.
  Defined.
  Definition SwitchMap {M:PreAdditive} (a b:M) (ab : BinDirectSum a b) (ba : BinDirectSum b a) : ab --> ba := π₁ · ι₂ + π₂ · ι₁.
  Lemma SwitchMapEqn {M:PreAdditive} {a b:M} (ab : BinDirectSum a b) (ba : BinDirectSum b a) : SwitchMap a b ab ba · SwitchMap b a ba ab = 1.
  Proof.
    unfold SwitchMap.
    rewrite <- to_BinOpId''.
    rewrite leftDistribute, 2 rightDistribute.
    rewrite assoc', (assoc ι₂). rewrite DirectSumIn2Pr1.
    rewrite zeroLeft, zeroRight, lunax.
    rewrite assoc', (assoc ι₂). rewrite (to_IdIn2 ba), id_left.
    apply maponpaths.
    rewrite assoc', (assoc ι₁). rewrite (to_IdIn1 ba), id_left.
    rewrite assoc', (assoc ι₁). rewrite DirectSumIn1Pr2.
    rewrite zeroLeft, zeroRight, runax.
    reflexivity.
  Defined.
  Definition SwitchIso {M:PreAdditive} (a b:M) (ab : BinDirectSum a b) (ba : BinDirectSum b a) : z_iso ab ba.
  Proof.
    ∃ (SwitchMap _ _ _ _). ∃ (SwitchMap _ _ _ _). split; apply SwitchMapEqn.
  Defined.
  Lemma SwitchMapEqnTo {M:PreAdditive} {a b c:M} (bc : BinDirectSum b c) (cb : BinDirectSum c b) (f:a-->b) (g:a-->c) :
    ToBinDirectSum bc f g · SwitchMap b c bc cb = ToBinDirectSum cb g f.
  Proof.
    unfold SwitchMap. apply ToBinDirectSumsEq.
    - rewrite rightDistribute. rewrite 2 assoc.
      rewrite 2 BinDirectSumPr1Commutes, BinDirectSumPr2Commutes.
      rewrite leftDistribute. rewrite 2 assoc'.
      rewrite (to_Unel2 cb).
      unfold to_unel.       rewrite zeroRight. rewrite lunax.
      rewrite (to_IdIn1 cb). rewrite id_right. reflexivity.
    - rewrite assoc'. rewrite leftDistribute. rewrite (assoc' π₂ _ π₂).
      rewrite (to_Unel1 cb). unfold to_unel. rewrite zeroRight. rewrite runax.
      rewrite 2 assoc. rewrite BinDirectSumPr1Commutes, BinDirectSumPr2Commutes.
      rewrite assoc'. rewrite (to_IdIn2 cb). rewrite id_right. reflexivity.
  Qed.
  Lemma SwitchMapMapEqn {M:PreAdditive} {a b c d:M}
        (ac : BinDirectSum a c) (ca : BinDirectSum c a)
        (bd : BinDirectSum b d) (db : BinDirectSum d b)
        (f : a --> b) (g : c --> d) :
    SwitchMap c a ca ac · directSumMap ac bd f g = directSumMap ca db g f · SwitchMap d b db bd.
  Proof.
    unfold SwitchMap.
    rewrite leftDistribute.
    rewrite assoc'. rewrite directSumMapEqIn2. rewrite assoc.
    rewrite rightDistribute. rewrite assoc. rewrite directSumMapEqPr1.
    apply maponpaths.
    rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc.
    rewrite assoc. rewrite directSumMapEqPr2.
    reflexivity.
  Qed.
  Definition directSumMapSwitch {M:PreAdditive} {a b c d:M}
        (ac : BinDirectSum a c) (ca : BinDirectSum c a)
        (bd : BinDirectSum b d) (db : BinDirectSum d b)
        (f : a --> b) (g : c --> d) :
    IsoArrow (directSumMap ac bd f g) (directSumMap ca db g f).
  Proof.
    ∃ (SwitchIso _ _ _ _). ∃ (SwitchIso _ _ _ _). apply SwitchMapMapEqn.
  Defined.
  Lemma opposite_directSumMap {M:PreAdditive} {a b c d:M}
        (ac : BinDirectSum a c) (bd : BinDirectSum b d)
        (f : a --> b) (g : c --> d) :
    directSumMap (M:=oppositePreAdditive M) (oppositeBinDirectSum bd) (oppositeBinDirectSum ac) (opp_mor f) (opp_mor g)
    =
    opp_mor (directSumMap ac bd f g).
  Proof.
    apply BinDirectSumIndArEq.
  Qed.
  Lemma opposite_directSumMap' {M:PreAdditive} {a b c d:M}
        (ac : BinDirectSum a c) (bd : BinDirectSum b d)
        (f : a --> b) (g : c --> d) :
    opp_mor (directSumMap (M:=oppositePreAdditive M) (oppositeBinDirectSum bd) (oppositeBinDirectSum ac) (opp_mor f) (opp_mor g))
    =
    directSumMap ac bd f g.
  Proof.
    apply (maponpaths opp_mor). apply opposite_directSumMap.
  Qed.
  Lemma SumOfKernels {M:PreAdditive} {x y z X Y Z : M}
        (xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
        (f : x --> y) (g : y --> z) (f' : X --> Y) (g' : Y --> Z) :
    isKernel' f g → isKernel' f' g' → isKernel' (directSumMap xX yY f f') (directSumMap yY zZ g g').
  Proof.
    intros i i'. split.
    { refine (BinDirectSumIndArComp _ _ _ _ _ _ _ _ @ ! _).
      apply ToBinDirectSumUnique.
      - exact (zeroLeft _ @ ! zeroRight _ @ maponpaths _ (! pr1 i)).
      - exact (zeroLeft _ @ ! zeroRight _ @ maponpaths _ (! pr1 i')). }
    intros w h e. apply iscontraprop1.
    2:{
      assert (e1 := ! assoc _ _ _
                      @ ! maponpaths (precomp_with _) directSumMapEqPr1
                      @ assoc _ _ _
                      @ maponpaths (postcomp_with _) e
                      @ zeroLeft _).
      assert (e2 := ! assoc _ _ _
                      @ ! maponpaths (precomp_with _) directSumMapEqPr2
                      @ assoc _ _ _
                      @ maponpaths (postcomp_with _) e
                      @ zeroLeft _).
      induction (iscontrpr1 (pr2 i w (h · π₁) e1)) as [h1 H1].
      induction (iscontrpr1 (pr2 i' w (h · π₂) e2)) as [h2 H2].
      ∃ (ToBinDirectSum _ h1 h2).
      apply ToBinDirectSumsEq.
      + refine (! assoc _ _ _ @ _ @ H1).
        refine (maponpaths (precomp_with _) directSumMapEqPr1 @ _).
        unfold precomp_with.
        refine (assoc _ _ _ @ _).
        apply (maponpaths (postcomp_with _)).
        apply BinDirectSumPr1Commutes.
      + refine (! assoc _ _ _ @ _ @ H2).
        refine (maponpaths (precomp_with _) directSumMapEqPr2 @ _).
        unfold precomp_with.
        refine (assoc _ _ _ @ _).
        apply (maponpaths (postcomp_with _)).
        apply BinDirectSumPr2Commutes. }
    apply invproofirrelevance.
    intros [k K] [k' K'].
    apply subtypeEquality_prop; cbn.
    apply ToBinDirectSumsEq.
    - refine (KernelIsMonic _ _ i _ _ _ _).
      exact (! assoc _ _ _
               @ ! maponpaths (precomp_with k) directSumMapEqPr1
               @ assoc _ _ _
               @ maponpaths (postcomp_with _) (K @ !K')
               @ ! assoc _ _ _
               @ maponpaths (precomp_with k') directSumMapEqPr1
               @ assoc _ _ _).
    - refine (KernelIsMonic _ _ i' _ _ _ _).
      exact (! assoc _ _ _
               @ ! maponpaths (precomp_with k) directSumMapEqPr2
               @ assoc _ _ _
               @ maponpaths (postcomp_with _) (K @ !K')
               @ ! assoc _ _ _
               @ maponpaths (precomp_with k') directSumMapEqPr2
               @ assoc _ _ _).
  Qed.
  Lemma SumOfCokernels {M:PreAdditive} {x y z X Y Z : M}
        (xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
        (f : x --> y) (g : y --> z) (f' : X --> Y) (g' : Y --> Z) :
    isCokernel' f g → isCokernel' f' g' → isCokernel' (directSumMap xX yY f f') (directSumMap yY zZ g g').
  Proof.
    intros i i'.
    rewrite <- (opposite_directSumMap' xX yY f f').
    rewrite <- (opposite_directSumMap' yY zZ g g').
    exact (SumOfKernels (M:=oppositePreAdditive M) (oppositeBinDirectSum zZ) (oppositeBinDirectSum yY) (oppositeBinDirectSum xX) g f g' f' i i').
  Qed.
  Lemma inducedMapReflectsKernels (M : PreAdditive) {X:Type} (j : X → ob M)
        {A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
    isKernel' (# (induced_PreAdditive_incl M j) i)
              (# (induced_PreAdditive_incl M j) p)
    →
    isKernel' i p.
  Proof.
    exact (λ k, pr1 k,,λ T h e, pr2 k (j T) h e).
  Qed.
  Lemma inducedMapReflectsCokernels (M : PreAdditive) {X:Type} (j : X → ob M)
        {A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
    isCokernel' (# (induced_PreAdditive_incl M j) i)
              (# (induced_PreAdditive_incl M j) p)
    →
    isCokernel' i p.
  Proof.
    exact (λ k, pr1 k,,λ T h e, pr2 k (j T) h e).
  Qed.
End PreAdditive.
Section KernelCokernelPairs.
  Definition isKernelCokernelPair {M :PreAdditive} {A B C:M} (i : A --> B) (p: B --> C) : hProp
    := isKernel' i p ∧ isCokernel' i p.
  Definition PairToKernel {M :PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
    isKernelCokernelPair i p → isKernel' i p := pr1.
  Definition PairToCokernel {M :PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
    isKernelCokernelPair i p → isCokernel' i p := pr2.
  Lemma inducedMapReflectsKernelCokernelPairs (M : PreAdditive) {X:Type} (j : X → ob M)
        {A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
    isKernelCokernelPair
      (# (induced_PreAdditive_incl M j) i)
      (# (induced_PreAdditive_incl M j) p)
    →
    isKernelCokernelPair i p.
  Proof.
    intros [k c]. split.
    - now apply inducedMapReflectsKernels.
    - now apply inducedMapReflectsCokernels.
  Qed.
  Definition opposite_isKernelCokernelPair {M:PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
    isKernelCokernelPair i p → isKernelCokernelPair (M:=oppositePreAdditive M) p i.
  Proof.
    intros s.
    split.
    - exact (PairToCokernel s).
    - exact (PairToKernel s).
  Defined.
  Lemma PairUniqueness1 {M :PreAdditive} {A A' B C:M} (i : A --> B) (i' : A' --> B) (p: B --> C) :
    isKernelCokernelPair i p → isKernelCokernelPair i' p → iscontr (IsoArrowTo i i').
  Proof.
    intros [k _] [k' _]. exact (KernelUniqueness k k').
  Defined.
  Lemma PairUniqueness2 {M :PreAdditive} {A B C C':M} (i : A --> B) (p: B --> C) (p': B --> C') :
    isKernelCokernelPair i p → isKernelCokernelPair i p' → iscontr (IsoArrowFrom p p').
  Proof.
    intros [_ c] [_ c']. exact (CokernelUniqueness c c').
  Defined.
  Lemma kerCokerDirectSum {M :PreAdditive} {A B:M} (S:BinDirectSum A B) : isKernelCokernelPair (to_In1 S) (to_Pr2 S).
  Proof.
    assert (E := BinDirectSum_isBinDirectSum M S).
    split.
    - ∃ (to_Unel1 S). intros T h H. use unique_exists; cbn beta.
      + exact (h · to_Pr1 S).
      + refine (! assoc _ _ _ @ _ @ id_right _). rewrite <- (to_BinOpId' S).
        rewrite rightDistribute. rewrite (assoc h (to_Pr2 S) (to_In2 S)).
        rewrite H; clear H. rewrite zeroLeft. apply pathsinv0. apply (runax (T-->S)).
      + intros k. apply to_has_homsets.
      + clear H. intros k e. induction e. rewrite assoc'.
        rewrite (to_IdIn1 S). apply pathsinv0, id_right.
    - ∃ (to_Unel1 S). intros T h H. use unique_exists; cbn beta.
      + exact (ι₂ · h).
      + refine (assoc _ _ _ @ _ @ id_left h). rewrite <- (to_BinOpId' S).
        rewrite leftDistribute.
        rewrite <- (assoc (to_Pr1 S) (to_In1 S) h). rewrite H; clear H.
        rewrite zeroRight. apply pathsinv0. apply (lunax (S-->T)).
      + intros k. apply to_has_homsets.
      + clear H. intros k e. induction e. rewrite assoc. rewrite (to_IdIn2 S).
        exact (! id_left _).
  Qed.
  Lemma kerCoker10 {M :PreAdditive} (Z:Zero M) (A:M) : isKernelCokernelPair (identity A) (0 : A --> Z).
  Proof.
    exact (kerCokerDirectSum (TrivialDirectSum Z A)).
  Qed.
  Lemma kerCoker01 {M :PreAdditive} (Z:Zero M) (A:M) : isKernelCokernelPair (0 : Z --> A) (identity A).
  Proof.
    exact (kerCokerDirectSum (TrivialDirectSum' Z A)).
  Qed.
  Lemma PairPushoutMap {M :PreAdditive} {A B C A':M} {i : A --> B} {p : B --> C}
        (pr : isKernelCokernelPair i p)
        (r : A --> A') (po : Pushout i r) :
    ∑ (q : po --> C), PushoutIn1 po · q = p × PushoutIn2 po · q = 0.
  Proof.
    refine (iscontrpr1 (isPushout_Pushout po C p 0 _)).
    refine (pr1 (PairToCokernel pr) @ ! _). apply zeroRight.
  Qed.
  Lemma PairPullbackMap {M :PreAdditive} {A B C A':M} {i : A <-- B} {p : B <-- C}
        (pr : isKernelCokernelPair p i)
        (r : A <-- A') (pb : Pullback i r) :
    ∑ (q : pb <-- C), PullbackPr1 pb ∘ q = p × PullbackPr2 pb ∘ q = 0.
  Proof.
    exact (PairPushoutMap (M:=oppositePreAdditive M) (opposite_isKernelCokernelPair pr) r pb).
  Defined.
  Lemma PairPushoutCokernel {M :PreAdditive} {A B C A':M} (i : A --> B) (p : B --> C)
        (pr : isKernelCokernelPair i p)
        (r : A --> A') (po : Pushout i r)
        (j := PushoutIn2 po)
        (pp := PairPushoutMap pr r po) :
    isCokernel' j (pr1 pp).
  Proof.
    set (s := PushoutIn1 po).
    induction pp as [q [e1 e2]]; change (isCokernel' j q);
      change (hProptoType (s · q = p)) in e1;
      change (hProptoType (j · q = 0)) in e2.
    ∃ e2.
    intros T h e.
    assert (L : i · (s · h) = 0).
    { refine (assoc _ _ _ @ _).
      intermediate_path (r · j · h).
      { apply (maponpaths (λ s, s · h)). exact (PushoutSqrCommutes po). }
      refine (! assoc _ _ _ @ _).
      induction (!e).
      apply zeroRight. }
    assert (V := iscontrpr1 ((pr22 pr) T (s · h) L)); clear L.
    induction V as [k e3].
    use iscontraprop1.
    { apply invproofirrelevance; intros φ φ'.
      apply subtypeEquality_prop.
      induction φ as [φ e4]; induction φ' as [φ' e5]; cbn.
      use (_ : isEpi q).
      { apply (isEpi_precomp M s q). rewrite e1. apply (CokernelIsEpi i p). apply pr. }
      exact (e4 @ ! e5). }
    ∃ k.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout po)); fold s j.
    { refine (assoc _ _ _ @ _ @ e3). apply (maponpaths (λ s, s · k)). exact e1. }
    { refine (assoc _ _ _ @ _ @ ! e). rewrite e2. apply zeroLeft. }
  Qed.
  Lemma PairPullbackKernel {M : PreAdditive} {A B C A':M} (i : A <-- B) (p : B <-- C)
        (pr : isKernelCokernelPair p i)
        (r : A <-- A') (pb : Pullback i r)
        (j := PullbackPr2 pb)
        (pp := PairPullbackMap pr r pb) :
    isKernel' (pr1 pp) j.
  Proof.
    exact (PairPushoutCokernel (M:=oppositePreAdditive M) i p (opposite_isKernelCokernelPair pr) r pb).
  Defined.
  Lemma SumOfKernelCokernelPairs {M : PreAdditive} {x y z X Y Z : M}
        (xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
        {f : x --> y} {g : y --> z} {f' : X --> Y} {g' : Y --> Z}
    : isKernelCokernelPair f g → isKernelCokernelPair f' g' → isKernelCokernelPair (directSumMap xX yY f f') (directSumMap yY zZ g g').
  Proof.
    intros i i'.
    ∃ (SumOfKernels _ _ _ f g f' g' (pr1 i) (pr1 i')).
    exact (SumOfCokernels _ _ _ f g f' g' (pr2 i) (pr2 i')).
  Qed.
End KernelCokernelPairs.

Section theDefinition.
  Definition ExactCategoryData := ∑ M:AdditiveCategory, MorphismPair M → hProp.   Coercion ExactCategoryDataToAdditiveCategory (ME : ExactCategoryData) : AdditiveCategory := pr1 ME.
  Definition isExact {M : ExactCategoryData} (E : MorphismPair M) : hProp := pr2 M E.
  Definition isExact2 {M : ExactCategoryData} {A B C:M} (f:A-->B) (g:B-->C) := isExact (mk_MorphismPair f g).
  Definition isAdmissibleMonomorphism {M : ExactCategoryData} {A B:M} (i : A --> B) : hProp :=
    ∃ C (p : B --> C), isExact2 i p.
  Definition AdmissibleMonomorphism {M : ExactCategoryData} (A B:M) : Type :=
    ∑ (i : A --> B), isAdmissibleMonomorphism i.
  Coercion AdmMonoToMap {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B → A --> B := pr1.
  Coercion AdmMonoToMap' {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B → (A --> B)%cat := pr1.
  Definition isAdmissibleEpimorphism {M : ExactCategoryData} {B C:M} (p : B --> C) : hProp :=
    ∃ A (i : A --> B), isExact2 i p.
  Definition AdmissibleEpimorphism {M : ExactCategoryData} (B C:M) : Type :=
    ∑ (p : B --> C), isAdmissibleEpimorphism p.
  Coercion AdmEpiToMap {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C → B --> C := pr1.
  Coercion AdmEpiToMap' {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C → (B --> C)%cat := pr1.
  Lemma ExactToAdmMono {M : ExactCategoryData} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isAdmissibleMonomorphism i.
  Proof.
    intros e. exact (hinhpr(C,,p,,e)).
  Qed.
  Lemma ExactToAdmEpi {M : ExactCategoryData} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isAdmissibleEpimorphism p.
  Proof.
    intros e. exact (hinhpr(A,,i,,e)).
  Qed.