Library UniMath.CategoryTheory.limits.kernels

Direct implementation of kernels

Contents

  • Definition of Kernel
  • Correspondence of Kernels and Equalizers
  • Kernel up to isomorphism
  • Kernel of morphism · Monic
  • KernelIn of equal morphisms
  • Transport of kernels

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.limits.equalizers.
Require Import UniMath.CategoryTheory.limits.zero.

Local Open Scope cat.

Definition of kernels
Section def_kernels.

  Context {C : category}.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

Definition and construction of Kernels
  Definition isKernel {x y z : C} (f : x --> y) (g : y --> z) (H : f · g = ZeroArrow Z x z) : UU :=
    ∏ (w : C) (h : w --> y) (H : h · g = ZeroArrow Z w z), ∃! φ : w --> x, φ · f = h.

  Lemma isKernel_paths {x y z : C} (f : x --> y) (g : y --> z) (H H' : f · g = ZeroArrow Z x z)
        (isK : isKernel f g H) : isKernel f g H'.
  Show proof.
    assert (e : H = H') by apply hs.
    induction e. exact isK.

  Definition make_isKernel {x y z : C} (f : x --> y) (g : y --> z) (H1 : f · g = ZeroArrow Z x z)
             (H2 : ∏ (w : C) (h : w --> y) (H' : h · g = ZeroArrow Z w z),
                   ∃! ψ : w --> x, ψ · f = h) : isKernel f g H1.
  Show proof.
    unfold isKernel.
    intros w h H.
    use unique_exists.
    - exact (pr1 (iscontrpr1 (H2 w h H))).
    - exact (pr2 (iscontrpr1 (H2 w h H))).
    - intros y0. apply hs.
    - intros y0 X. exact (base_paths _ _ (pr2 (H2 w h H) (tpair _ y0 X))).

  Definition Kernel {y z : C} (g : y --> z) : UU :=
    ∑ D : (∑ x : ob C, x --> y),
          ∑ (e : (pr2 D) · g = ZeroArrow Z (pr1 D) z), isKernel (pr2 D) g e.

  Definition make_Kernel {x y z : C} (f : x --> y) (g : y --> z) (H : f · g = ZeroArrow Z x z)
             (isE : isKernel f g H) : Kernel g := ((x,,f),,(H,,isE)).

  Definition Kernels : UU := ∏ (y z : C) (g : y --> z), Kernel g.

  Definition hasKernels : UU := ∏ (y z : C) (g : y --> z), ishinh (Kernel g).

Accessor functions
  Definition KernelOb {y z : C} {g : y --> z} (K : Kernel g) : C := pr1 (pr1 K).
  Coercion KernelOb : Kernel >-> ob.

  Definition KernelArrow {y z : C} {g : y --> z} (K : Kernel g) : C⟦K, y⟧ := pr2 (pr1 K).

  Definition KernelCompZero {y z : C} {g : y --> z} (K : Kernel g) :
    KernelArrow K · g = ZeroArrow Z K z := pr1 (pr2 K).

  Definition KernelisKernel {y z : C} {g : y --> z} (K : Kernel g) :
    isKernel (KernelArrow K) g (KernelCompZero K) := pr2 (pr2 K).

  Definition KernelIn {y z : C} {g : y --> z} (K : Kernel g) (w : C) (h : w --> y)
             (H : h · g = ZeroArrow Z w z) : C⟦w, K⟧ :=
    pr1 (iscontrpr1 ((KernelisKernel K) w h H)).

  Definition KernelCommutes {y z : C} {g : y --> z} (K : Kernel g) (w : C) (h : w --> y)
             (H : h · g = ZeroArrow Z w z) : (KernelIn K w h H) · (KernelArrow K) = h :=
    pr2 (iscontrpr1 ((KernelisKernel K) w h H)).

  Local Lemma KernelInUnique {x y z : C} {f : x --> y} {g : y --> z} {H : f · g = ZeroArrow Z x z}
        (isK : isKernel f g H) {w : C} {h : w --> y} (H' : h · g = ZeroArrow Z w z) {φ : w --> x}
        (H'' : φ · f = h) :
    φ = (pr1 (pr1 (isK w h H'))).
  Show proof.
    exact (base_paths _ _ (pr2 (isK w h H') (tpair _ φ H''))).

  Lemma KernelInsEq {y z: C} {g : y --> z} (K : Kernel g) {w : C} (φ1 φ2 : C⟦w, K⟧)
        (H : φ1 · (KernelArrow K) = φ2 · (KernelArrow K)) : φ1 = φ2.
  Show proof.
    assert (H1 : φ1 · (KernelArrow K) · g = ZeroArrow Z _ _).
    {
      rewrite <- assoc. rewrite KernelCompZero. apply ZeroArrow_comp_right.
    }
    rewrite (KernelInUnique (KernelisKernel K) H1 (idpath _)).
    apply pathsinv0.
    set (tmp := pr2 (KernelisKernel K w (φ1 · KernelArrow K) H1) (tpair _ φ2 (! H))).
    exact (base_paths _ _ tmp).

  Lemma KernelInComp {y z : C} {f : y --> z} (K : Kernel f) {x x' : C}
        (h1 : x --> x') (h2 : x' --> y)
        (H1 : h1 · h2 · f = ZeroArrow Z _ _) (H2 : h2 · f = ZeroArrow Z _ _) :
    KernelIn K x (h1 · h2) H1 = h1 · KernelIn K x' h2 H2.
  Show proof.
    use KernelInsEq. rewrite KernelCommutes. rewrite <- assoc. rewrite KernelCommutes.
    apply idpath.

Results on morphisms between Kernels.
  Definition identity_is_KernelIn {y z : C} {g : y --> z} (K : Kernel g) :
    ∑ φ : C⟦K, K⟧, φ · (KernelArrow K) = (KernelArrow K).
  Show proof.
    exists (identity K).
    apply id_left.

  Lemma KernelEndo_is_identity {y z : C} {g : y --> z} {K : Kernel g}
        (φ : C⟦K, K⟧) (H : φ · (KernelArrow K) = KernelArrow K) :
    identity K = φ.
  Show proof.
    set (H1 := tpair ((fun φ' : C⟦K, K⟧ => φ' · _ = _)) φ H).
    assert (H2 : identity_is_KernelIn K = H1).
    - apply proofirrelevancecontr.
      apply (KernelisKernel K).
      apply KernelCompZero.
    - apply (base_paths _ _ H2).

  Definition from_Kernel_to_Kernel {y z : C} {g : y --> z} (K K': Kernel g) : C⟦K, K'⟧.
  Show proof.
    apply (KernelIn K' K (KernelArrow K)). apply KernelCompZero.

  Lemma are_inverses_from_Kernel_to_Kernel {y z : C} {g : y --> z} (K K': Kernel g) :
    is_inverse_in_precat (from_Kernel_to_Kernel K K') (from_Kernel_to_Kernel K' K).
  Show proof.
    split.
    - apply pathsinv0. use KernelEndo_is_identity. rewrite <- assoc.
      unfold from_Kernel_to_Kernel. rewrite KernelCommutes.
      rewrite KernelCommutes. apply idpath.
    - apply pathsinv0. use KernelEndo_is_identity. rewrite <- assoc.
      unfold from_Kernel_to_Kernel. rewrite KernelCommutes.
      rewrite KernelCommutes. apply idpath.

  Lemma from_Kernel_to_Kernel_is_iso {y z : C} {g : y --> z} (K K' : Kernel g) :
    is_iso (from_Kernel_to_Kernel K K').
  Show proof.
    apply (is_iso_qinv _ (from_Kernel_to_Kernel K' K)).
    apply are_inverses_from_Kernel_to_Kernel.

  Definition iso_from_Kernel_to_Kernel {y z : C} {g : y --> z} (K K' : Kernel g) : z_iso K K' :=
    make_z_iso (from_Kernel_to_Kernel K K') (from_Kernel_to_Kernel K' K)
             (are_inverses_from_Kernel_to_Kernel K K').

Kernel of the ZeroArrow is given by identity
  Local Lemma KernelOfZeroArrow_isKernel (x y : C) :
    isKernel (identity x) (ZeroArrow Z x y) (id_left (ZeroArrow Z x y)).
  Show proof.
    use make_isKernel.
    intros w h H'.
    use unique_exists.
    - exact h.
    - cbn. apply id_right.
    - intros y0. apply hs.
    - intros y0 X. cbn in X. rewrite id_right in X. exact X.

  Definition KernelofZeroArrow (x y : C) : Kernel (@ZeroArrow C Z x y).
  Show proof.
    use make_Kernel.
    - exact x.
    - exact (identity x).
    - use id_left.
    - exact (KernelOfZeroArrow_isKernel x y).

Kernel of identity is given by arrow from zero
  Local Lemma KernelOfIdentity_isKernel (x : C) :
    isKernel (ZeroArrowFrom x) (identity x)
             (ArrowsFromZero C Z x (ZeroArrowFrom x · identity x) (ZeroArrow Z Z x)).
  Show proof.
    use make_isKernel.
    intros w h H'.
    use unique_exists.
    - exact (ZeroArrowTo w).
    - cbn. rewrite id_right in H'. rewrite H'. apply idpath.
    - intros y. apply hs.
    - intros y X. cbn in X. use ArrowsToZero.

  Definition KernelOfIdentity (x : C) : Kernel (identity x).
  Show proof.
    use make_Kernel.
    - exact Z.
    - exact (ZeroArrowFrom x).
    - use ArrowsFromZero.
    - exact (KernelOfIdentity_isKernel x).

More generally, the KernelArrow of the kernel of the ZeroArrow is an isomorphism.
  Lemma KernelofZeroArrow_is_iso {x y : C} (K : Kernel (ZeroArrow Z x y)) :
    is_inverse_in_precat (KernelArrow K) (from_Kernel_to_Kernel (KernelofZeroArrow x y) K).
  Show proof.
    use make_is_inverse_in_precat.
    - use KernelInsEq. rewrite <- assoc. unfold from_Kernel_to_Kernel. rewrite KernelCommutes.
      rewrite id_left. cbn. rewrite id_right. apply idpath.
    - unfold from_Kernel_to_Kernel. rewrite KernelCommutes. apply idpath.

  Definition KernelofZeroArrow_iso (x y : C) (K : Kernel (@ZeroArrow C Z x y)) : z_iso K x :=
    make_z_iso (KernelArrow K) (from_Kernel_to_Kernel (KernelofZeroArrow x y) K)
             (KernelofZeroArrow_is_iso K).

It follows that KernelArrow is monic.
  Lemma KernelArrowisMonic {y z : C} {g : y --> z} (K : Kernel g) : isMonic (KernelArrow K).
  Show proof.
    apply make_isMonic.
    intros z0 g0 h X.
    use KernelInsEq.
    exact X.

  Lemma KernelsIn_is_iso {x y : C} {f : x --> y} (K1 K2 : Kernel f) :
    is_iso (KernelIn K1 K2 (KernelArrow K2) (KernelCompZero K2)).
  Show proof.
    use is_iso_qinv.
    - use KernelIn.
      + use KernelArrow.
      + use KernelCompZero.
    - split.
      + use KernelInsEq. rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes.
        rewrite id_left. apply idpath.
      + use KernelInsEq. rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes.
        rewrite id_left. apply idpath.

End def_kernels.
Arguments KernelArrow [C] [Z] [y] [z] [g] _.

Correspondence of kernels and equalizers

Section kernel_equalizers.

  Context (C : category).
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

Equalizer from Kernel

  Lemma KernelEqualizer_eq {x y : ob C} {f : x --> y} (K : Kernel Z f) :
    KernelArrow K · f = KernelArrow K · ZeroArrow Z x y.
  Show proof.
    rewrite ZeroArrow_comp_right. apply KernelCompZero.

  Lemma KernelEqualizer_isEqualizer {x y : ob C} {f : x --> y} (K : Kernel Z f) :
    isEqualizer f (ZeroArrow Z x y) (KernelArrow K) (KernelEqualizer_eq K).
  Show proof.
    use make_isEqualizer.
    intros w h H'.
    use unique_exists.
    - use KernelIn.
      + exact h.
      + rewrite ZeroArrow_comp_right in H'. exact H'.
    - cbn. use KernelCommutes.
    - intros y0. apply hs.
    - intros y0 X. use KernelInsEq. rewrite KernelCommutes. exact X.

  Definition KernelEqualizer {x y : ob C} {f : x --> y} (K : Kernel Z f) :
    Equalizer f (ZeroArrow Z _ _).
  Show proof.
    use make_Equalizer.
    - exact K.
    - exact (KernelArrow K).
    - exact (KernelEqualizer_eq K).
    - exact (KernelEqualizer_isEqualizer K).

Kernel from Equalizer

  Lemma EqualizerKernel_eq {x y : ob C} {f : x --> y} (E : Equalizer f (ZeroArrow Z _ _)) :
    EqualizerArrow E · f = ZeroArrow Z E y.
  Show proof.
    rewrite <- (ZeroArrow_comp_right _ _ _ _ _ (EqualizerArrow E)).
    exact (EqualizerEqAr E).

  Lemma EqualizerKernel_isKernel {x y : ob C} {f : x --> y} (E : Equalizer f (ZeroArrow Z _ _)) :
    isKernel Z (EqualizerArrow E) f (EqualizerKernel_eq E).
  Show proof.
    use (make_isKernel).
    intros w h H'.
    use unique_exists.
    - use EqualizerIn.
      + exact h.
      + rewrite ZeroArrow_comp_right. exact H'.
    - use EqualizerCommutes.
    - intros y0. apply hs.
    - intros y0 X. use EqualizerInsEq. rewrite EqualizerCommutes. exact X.

  Definition EqualizerKernel {x y : ob C} {f : x --> y} (E : Equalizer f (ZeroArrow Z _ _)) :
    Kernel Z f.
  Show proof.
    use make_Kernel.
    - exact E.
    - exact (EqualizerArrow E).
    - exact (EqualizerKernel_eq E).
    - exact (EqualizerKernel_isKernel E).

End kernel_equalizers.

Kernel up to isomorphism

Section kernels_iso.

  Variable C : category.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

  Definition Kernel_up_to_iso_eq {x y z : C} (f : x --> y) (g : y --> z)
             (K : Kernel Z g) (h : z_iso x K) (H : f = h · (KernelArrow K)) :
    f · g = ZeroArrow Z x z.
  Show proof.
    induction K as [t p]. induction t as [t' p']. induction p as [t'' p''].
    unfold isEqualizer in p''.
    rewrite H.
    rewrite <- (ZeroArrow_comp_right _ _ _ _ _ h).
    rewrite <- assoc.
    apply cancel_precomposition.
    apply KernelCompZero.

  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''.
  Show 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.

  Definition Kernel_up_to_iso {x y z : C} (f : x --> y) (g : y --> z) (K : Kernel Z g)
             (h : z_iso x K) (H : f = h · (KernelArrow K)) : Kernel Z g :=
    make_Kernel Z f _ (Kernel_up_to_iso_eq f g K h H)
              (Kernel_up_to_iso_isKernel f g K h H (Kernel_up_to_iso_eq f g K h H)).

  Lemma Kernel_up_to_iso2_eq {x y z : C} {f1 : x --> y} {f2 : x --> z} (h : z_iso y z)
        (H : f1 · h = f2) (K : Kernel Z f1) : KernelArrow K · f2 = ZeroArrow Z K z.
  Show proof.
    rewrite <- H. rewrite assoc. rewrite KernelCompZero.
    apply ZeroArrow_comp_left.

  Definition Kernel_up_to_iso2_isKernel {x y z : C} (f1 : x --> y) (f2 : x --> z)
             (h : z_iso y z) (H : f1 · h = f2) (K : Kernel Z f1) :
    isKernel Z (KernelArrow K) f2 (Kernel_up_to_iso2_eq h H K).
  Show proof.
    use make_isKernel.
    intros w h0 H'.
    use unique_exists.
    - use KernelIn.
      + exact h0.
      + rewrite <- H in H'. rewrite <- (ZeroArrow_comp_left _ _ _ _ _ h) in H'.
        rewrite assoc in H'. apply (post_comp_with_z_iso_is_inj h) in H'.
        exact H'.
    - cbn. use KernelCommutes.
    - intros y0. apply hs.
    - intros y0 H''. use KernelInsEq.
      rewrite H''. apply pathsinv0.
      apply KernelCommutes.

  Definition Kernel_up_to_iso2 {x y z : C} {f1 : x --> y} {f2 : x --> z} {h : z_iso y z}
             (H : f1 · h = f2) (K : Kernel Z f1) : Kernel Z f2 :=
    make_Kernel Z (KernelArrow K) _ (Kernel_up_to_iso2_eq h H K)
              (Kernel_up_to_iso2_isKernel f1 f2 h H K).

End kernels_iso.

Kernel of morphism · monic

Introduction

Suppose f : x --> y is a morphism and M : y --> z is a Monic. Then kernel of f · M is isomorphic to kernel of f.
Section kernels_monics.

  Variable C : category.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

  Local Lemma KernelCompMonic_eq1 {x y z : C} (f : x --> y) (M : Monic C y z)
        (K1 : Kernel Z (f · M)) (K2 : Kernel Z f) :
    KernelArrow K1 · f = ZeroArrow Z K1 y.
  Show proof.
    use (MonicisMonic C M). rewrite ZeroArrow_comp_left. rewrite <- assoc. use KernelCompZero.

  Definition KernelCompMonic_mor1 {x y z : C} (f : x --> y) (M : Monic C y z)
        (K1 : Kernel Z (f · M)) (K2 : Kernel Z f) : C⟦K1, K2⟧ :=
    KernelIn Z K2 _ (KernelArrow K1) (KernelCompMonic_eq1 f M K1 K2).

  Local Lemma KernelCompMonic_eq2 {x y z : C} (f : x --> y) (M : Monic C y z)
        (K1 : Kernel Z (f · M)) (K2 : Kernel Z f) : KernelArrow K2 · (f · M) = ZeroArrow Z K2 z.
  Show proof.
    rewrite assoc. rewrite KernelCompZero. apply ZeroArrow_comp_left.

  Definition KernelCompMonic_mor2 {x y z : C} (f : x --> y) (M : Monic C y z)
             (K1 : Kernel Z (f · M)) (K2 : Kernel Z f) : C⟦K2, K1⟧ :=
    KernelIn Z K1 _ (KernelArrow K2) (KernelCompMonic_eq2 f M K1 K2).

  Lemma KernelCompMonic1 {x y z : C} (f : x --> y) (M : Monic C y z)
             (K1 : Kernel Z (f · M)) (K2 : Kernel Z f) :
    is_iso (KernelCompMonic_mor1 f M K1 K2).
  Show proof.
    use is_iso_qinv.
    - exact (KernelCompMonic_mor2 f M K1 K2).
    - split.
      + unfold KernelCompMonic_mor1. unfold KernelCompMonic_mor2.
        use KernelInsEq.
        rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes.
        apply pathsinv0. apply id_left.
      + unfold KernelCompMonic_mor1. unfold KernelCompMonic_mor2.
        use KernelInsEq.
        rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes.
        apply pathsinv0. apply id_left.

  Lemma KernelCompMonic2 {x y z : C} (f : x --> y) (M : Monic C y z)
             (K1 : Kernel Z (f · M)) (K2 : Kernel Z f) :
    is_iso (KernelCompMonic_mor2 f M K1 K2).
  Show proof.
    use is_iso_qinv.
    - exact (KernelCompMonic_mor1 f M K1 K2).
    - split.
      + unfold KernelCompMonic_mor1. unfold KernelCompMonic_mor2.
        use KernelInsEq.
        rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes.
        apply pathsinv0. apply id_left.
      + unfold KernelCompMonic_mor1. unfold KernelCompMonic_mor2.
        use KernelInsEq.
        rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes.
        apply pathsinv0. apply id_left.

  Local Lemma KernelCompMonic_eq {x y z : C} (f : x --> y) (M : Monic C y z)
        (K : Kernel Z (f · M)) : KernelArrow K · f = ZeroArrow Z K y.
  Show proof.
    use (MonicisMonic C M). rewrite ZeroArrow_comp_left. rewrite <- assoc. use KernelCompZero.

  Lemma KernelCompMonic_isKernel {x y z : C} (f : x --> y) (M : Monic C y z)
        (K : Kernel Z (f · M)) :
    isKernel Z (KernelArrow K) f (KernelCompMonic_eq f M K).
  Show proof.
    use make_isKernel.
    - intros w h H'.
      use unique_exists.
      + use KernelIn.
        * exact h.
        * rewrite assoc. rewrite <- (ZeroArrow_comp_left _ _ _ _ _ M). apply cancel_postcomposition.
          exact H'.
      + cbn. rewrite KernelCommutes. apply idpath.
      + intros y0. apply hs.
      + intros y0 X.
        apply pathsinv0. cbn in X.
        use (MonicisMonic C (make_Monic _ _ (KernelArrowisMonic Z K))). cbn.
        rewrite KernelCommutes. apply pathsinv0. apply X.

  Definition KernelCompMonic {x y z : C} (f : x --> y) (M : Monic C y z) (K : Kernel Z (f · M)) :
    Kernel Z f.
  Show proof.
    use make_Kernel.
    - exact K.
    - use KernelArrow.
    - exact (KernelCompMonic_eq f M K).
    - exact (KernelCompMonic_isKernel f M K).

End kernels_monics.

KernelIn of equal, not necessarily definitionally equal, morphisms is iso

Section kernel_in_paths.

  Variable C : category.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

  Definition KernelInPaths_is_iso_mor {x y : C} {f f' : x --> y} (e : f = f')
             (K1 : Kernel Z f) (K2 : Kernel Z f') : K1 --> K2.
  Show proof.
    induction e.
    use KernelIn.
    - use KernelArrow.
    - use KernelCompZero.

  Lemma KernelInPaths_is_iso {x y : C} {f f' : x --> y} (e : f = f')
        (K1 : Kernel Z f) (K2 : Kernel Z f') : is_iso (KernelInPaths_is_iso_mor e K1 K2).
  Show proof.
    induction e. apply KernelsIn_is_iso.

  Local Lemma KernelPath_eq {x y : C} {f f' : x --> y} (e : f = f') (K : Kernel Z f) :
    KernelArrow K · f' = ZeroArrow Z K y.
  Show proof.
    induction e. use KernelCompZero.

  Local Lemma KernelPath_isKernel {x y : C} {f f' : x --> y} (e : f = f') (K : Kernel Z f) :
    isKernel Z (KernelArrow K) f' (KernelPath_eq e K).
  Show proof.
    induction e. use KernelisKernel.

Constructs a cokernel of f' from a cokernel of f in a natural way
  Definition KernelPath {x y : C} {f f' : x --> y} (e : f = f') (K : Kernel Z f) : Kernel Z f'.
  Show proof.
    use make_Kernel.
    - exact K.
    - use KernelArrow.
    - exact (KernelPath_eq e K).
    - exact (KernelPath_isKernel e K).

End kernel_in_paths.

Transports of kernels

Section transport_kernels.

  Variable C : category.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

  Local Lemma transport_source_KernelIn_eq {x' x y z : C} (f : x --> y) {g : y --> z}
        (K : Kernel Z g) (e : x = x') (H : f · g = ZeroArrow Z _ _) :
    (transportf (λ x' : ob C, precategory_morphisms x' y) e f) · g = ZeroArrow Z _ _.
  Show proof.
    induction e. apply H.

  Lemma transport_source_KernelIn {x' x y z : C} (f : x --> y) {g : y --> z} (K : Kernel Z g)
        (e : x = x') (H : f · g = ZeroArrow Z _ _) :
    transportf (λ x' : ob C, precategory_morphisms x' K) e (KernelIn Z K _ f H) =
    KernelIn Z K _ (transportf (λ x' : ob C, precategory_morphisms x' y) e f)
             (transport_source_KernelIn_eq f K e H).
  Show proof.
    induction e. use KernelInsEq. cbn.
    rewrite KernelCommutes. rewrite KernelCommutes.
    apply idpath.

End transport_kernels.