Lemma IsomorphicToSplit {M:PreAdditive} (P Q : MorphismPair M) : MorphismPairIsomorphism P Q ⇒ isSplit P ⇒ isSplit Q. Proof. intros [f' [f [f'' [[e _] [e' _]]]]] ex. apply (squash_to_hProp ex); clear ex; intros [q [j su]]; apply hinhpr. exists (z_iso_inv f · q · f'). exists (z_iso_inv f'' · j · f). split. { intermediate_path (z_iso_inv f' · Mor1 P · q · f'). { rewrite 2 assoc. apply (maponpaths (λ k, k·f')). apply (maponpaths (λ k, k·q)). apply pathsinv0. apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. exact e. } { rewrite 2 assoc'. rewrite (assoc _ q _). intermediate_path (z_iso_inv f' · (identity _ · f')). { apply maponpaths. apply (maponpaths (λ k, k·f')). exact (to_IdIn1 su). } { rewrite id_left. apply z_iso_after_z_iso_inv. } } } split. { rewrite assoc'. rewrite e'. rewrite assoc. rewrite (assoc' _ j _). apply wrap_inverse. apply (to_IdIn2 su). } split. { assert (r := to_Unel1 su); unfold to_unel in r. assert (r' := maponpaths (λ t, t · f'') r); cbn in r'; clear r. rewrite assoc' in r'. rewrite <- e' in r'. rewrite assoc in r'. rewrite <- e in r'. assert (r'' := maponpaths (λ t, z_iso_inv f' · t) r'); clear r'; cbn in r''. rewrite 2 assoc in r''. rewrite z_iso_after_z_iso_inv in r''. rewrite assoc' in r''. rewrite id_left in r''. rewrite zeroLeft,zeroRight in r''. exact r''. } split. { rewrite 2 assoc. rewrite (assoc' _ f _). rewrite z_iso_inv_after_z_iso. rewrite id_right. rewrite (assoc' _ j _). rewrite (to_Unel2 su). unfold to_unel. rewrite zeroRight, zeroLeft. reflexivity. } { apply (cancel_z_iso' f). rewrite id_right. rewrite rightDistribute. rewrite 3 (assoc f). rewrite z_iso_inv_after_z_iso, id_left. rewrite assoc'. rewrite e. rewrite assoc. rewrite (assoc f). rewrite e'. rewrite (assoc' _ f''). rewrite 2 (assoc f''). rewrite z_iso_inv_after_z_iso, id_left. rewrite assoc. rewrite <- leftDistribute. rewrite (to_BinOpId' su). rewrite id_left. 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). } } }