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.
Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Isos. Definition IsoArrowFrom {M : category}   {A B B':M} (g : A --> B) (g' : A --> B') := ∑ i : z_iso B B', g · i  = g'. Coercion IsoArrowFrom_pr1 {M : category} {A B B':M} (g : A --> B) (g' : A --> B') : IsoArrowFrom g g' -> z_iso B B' := pr1. IsoArrowTo g g' -> IsoArrowFrom (M:=M^op) g' g. Definition opposite_IsoArrowFrom {M:category} {A B B':M} {g : A --> B} {g' : A --> B'} : IsoArrowFrom g g' -> IsoArrowTo (M:=M^op) g' g. Lemma IsoArrowFrom_isaprop (M : category) {A B B':M} (g : A --> B) (g' : A --> B') : isEpi g -> isaprop (IsoArrowFrom g g'). isCokernel' f g -> isCokernel' f g' -> iscontr (IsoArrowFrom g g'). - exact (IsoArrowFrom_isaprop M g g' (CokernelIsEpi f g i)). + apply ArrowsFromZero. isKernelCokernelPair i p -> isKernelCokernelPair i p' -> iscontr (IsoArrowFrom p p'). Lemma ExactSequenceFromMono {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) : Lemma ExactSequenceFromEpi {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) : exact (ExactSequenceFromMono (M:=M^op) p i). exact (ExactSequenceFromMono _ _ (pr2 (kerCoker10 Z A)) (EC_IdentityIsMono A)). exact (ExactSequenceFromEpi _ _ (pr1 (kerCoker01 Z A)) (EC_IdentityIsEpi A)). Lemma FromZeroIsMono {M : ExactCategory} (Z:Zero M) (A:M) : isAdmissibleMonomorphism (0 : Z --> A). Definition MonoFromZero {M : ExactCategory} (Z:Zero M) (A:M) : Z ↣ A := (0 : Z --> A),,FromZeroIsMono Z A. Goal ∏ (M:ExactCategory) (A:M) (Z:Zero M), EpiToZero A Z = MonoFromZero (M:=M^op) (Zero_opp M Z) A. IsoArrowFrom f f' -> isAdmissibleMonomorphism f -> isAdmissibleMonomorphism f'. use ExactSequenceFromEpi. exists po. use ExactSequenceFromMono. { use ExactSequenceFromMono. exists pb. use ExactSequenceFromEpi. { use ExactSequenceFromEpi. apply hinhpr. exists D. exists (π₁ · p). apply ExactSequenceFromEpi. intros i i'. apply ExactSequenceFromMono. assert (Q := r' @ ! s'); clear r' s' u h. apply FromBinDirectSumsEq. Lemma AdmMonoFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : assert (es := ExactSequenceFromMono _ _ co); clear co. use (ExactToAdmMono (p:=k)). use (ExactSequenceFromEpi i k). Lemma AdmEpiFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : exact (AdmMonoFromComposite (M:=M^op) j i). assert (ijs := ExactSequenceFromMono (i·j) s L IJ). { use (ExactSequenceFromMono k u _ K). exists e4. intros T h e0. { exact (@AdmMonoFromComposite M). } { exact (@AdmEpiFromComposite M). } } }