proposition: Lemma CoIm_to_Im_is_iso {x y : A} (f : x --> y) : is_z_isomorphism (CoIm_to_Im f).
proof: Proof. use monic_epi_is_iso. - use (isMonic_postcomp A _ (KernelArrow (Image f))). intros z g1 g2 H. set (q := Coequalizer A g1 g2). set (ar := CoIm_to_Im f · KernelArrow (Image f)). set (ar1 := CoequalizerOut q _ ar). set (com1 := CoequalizerCommutes q _ _ H). assert (isE : isEpi ((CokernelArrow (CoImage f)) · (CoequalizerArrow q))). { apply isEpi_comp. apply CokernelArrowisEpi. apply CoequalizerArrowisEpi. } set (E := make_Epi A ((CokernelArrow (CoImage f)) · (CoequalizerArrow q)) isE). set (coker := EpiToCokernel E). assert (e0 : (KernelArrow (to_Kernels A _ _ E)) · ((CokernelArrow (CoImage f)) · (CoequalizerArrow q)) = ZeroArrow (to_Zero A) _ (EpiToCokernel E)). { set (tmp := CokernelCompZero (to_Zero A) (EpiToCokernel E)). rewrite <- tmp. apply cancel_precomposition. unfold E. apply idpath. } assert (e : (KernelArrow (to_Kernels A _ _ E)) · f = ZeroArrow (to_Zero A) _ _). { set (tmp := CoIm_to_Im_eq f). apply (maponpaths (λ f : _, (KernelArrow (to_Kernels A _ _ E)) · f)) in tmp. use (pathscomp0 tmp). rewrite <- assoc. rewrite <- com1. rewrite assoc. rewrite assoc. set (tmpar1 := CoIm_to_Im f · KernelArrow (Image f)). set (tmpar2 := CoequalizerOut q y tmpar1 H). rewrite <- (ZeroArrow_comp_left A (to_Zero A) _ _ _ tmpar2). apply cancel_postcomposition. rewrite <- assoc. rewrite e0. apply idpath. } set (l := KernelIn (to_Zero A) (Kernel f) _ _ e). assert (e1 : (KernelArrow (to_Kernels A _ _ E)) · (CokernelArrow (CoImage f)) = ZeroArrow (to_Zero A) _ _). { set (tmp := KernelCommutes (to_Zero A) (Kernel f) _ _ e). rewrite <- tmp. fold l. rewrite <- (ZeroArrow_comp_right A (to_Zero A) _ _ _ l). rewrite <- assoc. apply cancel_precomposition. unfold CoImage. apply CokernelCompZero. } set (ar2 := CokernelOut (to_Zero A) coker _ _ e1). set (com2 := CokernelCommutes (to_Zero A) coker _ _ e1). assert (e2 : CokernelArrow (CoImage f) · (CoequalizerArrow q) · (CokernelOut (to_Zero A) coker _ _ e1) = CokernelArrow (CoImage f)). { apply com2. } assert (e3 : (CoequalizerArrow q) · (CokernelOut (to_Zero A) coker (CoImage f) _ e1) = identity _). { set (isE1 := CokernelArrowisEpi (to_Zero A) (CoImage f)). unfold isEpi in isE1. apply isE1. rewrite assoc. rewrite id_right. apply e2. } assert (e4 : isMonic (CoequalizerArrow q)). { apply (isMonic_postcomp A _ (CokernelOut (to_Zero A) coker (CoImage f) _ e1)). set (tmp := @identity_isMonic A (CoImage f)). rewrite <- e3 in tmp. apply tmp. } set (coeqeq := CoequalizerEqAr q). apply e4 in coeqeq. apply coeqeq. - use (isEpi_precomp A (CokernelArrow (CoImage f)) _). intros z g1 g2 H. set (q := Equalizer A g1 g2). set (ar := CokernelArrow (CoImage f) · CoIm_to_Im f). set (ar1 := EqualizerIn q _ ar). set (com1 := EqualizerCommutes q _ _ H). assert (isE : isMonic ((EqualizerArrow q) · (KernelArrow (Image f)))). { apply isMonic_comp. apply EqualizerArrowisMonic. apply KernelArrowisMonic. } set (M := make_Monic A ((EqualizerArrow q) · (KernelArrow (Image f))) isE). set (ker := MonicToKernel M). assert (e0 : (EqualizerArrow q) · (KernelArrow (Image f)) · (CokernelArrow (to_Cokernels A _ _ M)) = ZeroArrow (to_Zero A) (MonicToKernel M) _). { use (pathscomp0 _ (KernelCompZero (to_Zero A) (MonicToKernel M))). apply cancel_precomposition. apply idpath. } assert (e : f · (CokernelArrow (to_Cokernels A _ _ M)) = ZeroArrow (to_Zero A) _ _). { set (tmp := CoIm_to_Im_eq f). apply (maponpaths (λ f : _, f · (CokernelArrow (to_Cokernels A _ _ M)))) in tmp. use (pathscomp0 tmp). rewrite <- com1. set (tmpar1 := CokernelArrow (CoImage f) · CoIm_to_Im f). set (tmpar2 := EqualizerIn q x tmpar1 H). rewrite <- (ZeroArrow_comp_right A (to_Zero A) _ _ _ tmpar2). rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite assoc. rewrite e0. apply idpath. } set (l := CokernelOut (to_Zero A) (Cokernel f) _ _ e). assert (e1 : (KernelArrow (Image f)) · (CokernelArrow (to_Cokernels A _ _ M)) = ZeroArrow (to_Zero A) _ _). { set (tmp := CokernelCommutes (to_Zero A) (Cokernel f) _ _ e). rewrite <- tmp. fold l. rewrite <- (ZeroArrow_comp_left A (to_Zero A) _ _ _ l). rewrite assoc. apply cancel_postcomposition. unfold Image. apply KernelCompZero. } set (ar2 := KernelIn (to_Zero A) ker _ _ e1). set (com2 := KernelCommutes (to_Zero A) ker _ _ e1). assert (e2 : (KernelIn (to_Zero A) ker _ _ e1) · (EqualizerArrow q) · KernelArrow (Image f) = KernelArrow (Image f)). { rewrite <- com2. rewrite <- assoc. apply cancel_precomposition. unfold ker. apply idpath. } assert (e3 : (KernelIn (to_Zero A) ker (Image f) _ e1) · (EqualizerArrow q) = identity _). { set (isM1 := KernelArrowisMonic (to_Zero A) (Image f)). unfold isMonic in isM1. apply isM1. rewrite id_left. apply e2. } assert (e4 : isEpi (EqualizerArrow q)). { apply (isEpi_precomp A (KernelIn (to_Zero A) ker (Image f) _ e1)). set (tmp := @identity_isEpi A (Image f)). rewrite <- e3 in tmp. apply tmp. } set (eqeq := EqualizerEqAr q). apply e4 in eqeq. apply eqeq. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive