proposition: Lemma CokernelSequence {M:ExactCategory} {A B C P R:M} (i : A --> B) (j : B --> C) (p : B --> P) (q : C --> R) : isExact2 i p -> isExact2 j q -> ∃ Q (s : C --> Q) (k : P --> Q) (r : Q --> R), isExact2 (i·j) s ∧ isExact2 k r ∧ isPushout' (M:=M) j p s k ∧ s · r = q.
proof: Proof. intros ip jq. assert (co := EC_ExactToCokernel ip : isCokernel' i p). assert (b := EC_ExactToCokernel jq : isCokernel' j q). assert (I := ExactToAdmMono ip). assert (J := ExactToAdmMono jq). assert (IJ := EC_ComposeMono _ _ I J). induction b as [a co']. assert (ijq : i · (j · q) = 0). { rewrite a. apply zeroRight. } assert (po := EC_PushoutMono j p (ExactToAdmMono jq)). use (hinhfun _ po); clear po; intros [[[Q [s k]] [e1 po]] K]. change (isPushout j p s k e1) in po; change (hProptoType (isAdmissibleMonomorphism k)) in K; change (hProptoType (j · s = p · k)) in e1. assert (L := PushoutCokernel _ _ _ _ _ co (_,,po)). exists Q. exists s. exists k. assert (e2 : j · q = p · 0). { rewrite a. now rewrite zeroRight. } assert (PO := iscontrpr1 (po R q 0 e2)). induction PO as [u [e3 e4]]. exists u. assert (ijs := ExactSequenceFromMono (i·j) s L IJ). exists ijs. split. { use (ExactSequenceFromMono k u _ K). exists e4. intros T h e0. assert (e5 : j · (s · h) = 0). { rewrite assoc. rewrite e1. rewrite assoc'. rewrite e0. now rewrite zeroRight. } assert (W := co' T (s·h) e5); cbn in W. use (iscontrweqf _ W). apply weqfibtototal; intros l. apply weqiff. rewrite <- e3. rewrite assoc'. split. { intros e. now apply (CokernelIsEpi (i·j) s (EC_ExactToCokernel ijs)). } { intros e. now apply maponpaths. } + apply to_has_homsets. + apply to_has_homsets. } split. - exists e1. exact po. - exact e3. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions