proposition: Lemma Kernel_up_to_iso_isKernel {x y z : C} (f : x --> y) (g : y --> z) (K : Kernel Z g) (h : z_iso x K) (H : f = h · (KernelArrow K)) (H'' : f · g = ZeroArrow Z x z) : isKernel Z f g H''.
proof: Proof. use make_isKernel. intros w h0 H'. use unique_exists. - exact (KernelIn Z K w h0 H' · inv_from_z_iso h). - cbn beta. rewrite H. rewrite assoc. rewrite <- (assoc _ _ h). cbn. rewrite (is_inverse_in_precat2 h). rewrite id_right. apply KernelCommutes. - intros y0. apply hs. - intros y0 X. cbn beta in X. use (post_comp_with_z_iso_is_inj h). rewrite <- assoc. use (pathscomp0 _ (! (maponpaths (λ gg : _, KernelIn Z K w h0 H' · gg) (is_inverse_in_precat2 h)))). rewrite id_right. use KernelInsEq. rewrite KernelCommutes. rewrite <- X. rewrite <- assoc. apply cancel_precomposition. apply pathsinv0. apply H. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Zero