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.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.limits.graphs.zero.
Require Import UniMath.CategoryTheory.limits.graphs.equalizers.
Require Import UniMath.CategoryTheory.limits.kernels.

Section def_kernels.

  Variable C : precategory.
  Variable hs: has_homsets C.
  Variable Z : Zero C.

  Definition Kernel {a b : C} (f : C⟦a, b⟧) := Equalizer C f (ZeroArrow Z a b).

  Lemma equiv_Kernel1_eq {a b : C} (f : C⟦a, b⟧) (K : limits.kernels.Kernel (equiv_Zero2 Z) f) :
    KernelArrow K · f = KernelArrow K · ZeroArrow Z a b.
  Proof.
    rewrite precomp_with_ZeroArrow. rewrite <- equiv_ZeroArrow. apply KernelCompZero.
  Qed.

  Lemma equiv_Kernel1_isEqualizer {a b : C} (f : C⟦a, b⟧)
        (K : limits.kernels.Kernel (equiv_Zero2 Z) f) :
    isEqualizer C f (ZeroArrow Z a b) K (KernelArrow K) (equiv_Kernel1_eq f K).
  Proof.
    use (make_isEqualizer _ hs).
    intros e h' H'.
    use unique_exists.
    - use KernelIn.
      + exact h'.
      + rewrite precomp_with_ZeroArrow in H'.
        use (pathscomp0 _ (!(equiv_ZeroArrow e b Z))).
        exact H'.
    - cbn. use KernelCommutes.
    - intros y. apply hs.
    - intros y X. cbn in X.
      use limits.kernels.KernelInsEq. unfold KernelArrow.
      use (pathscomp0 X). apply pathsinv0.
      use limits.kernels.KernelCommutes.
  Qed.

  Definition equiv_Kernel1 {a b : C} (f : C⟦a, b⟧) (K : limits.kernels.Kernel (equiv_Zero2 Z) f) :
    Kernel f.
  Proof.
    use make_Equalizer.
    - exact K.
    - exact (KernelArrow K).
    - exact (equiv_Kernel1_eq f K).
    - exact (equiv_Kernel1_isEqualizer f K).
  Defined.


  Lemma equiv_Kernel2_eq {a b : C} (f : C⟦a, b⟧) (K : Kernel f) :
    EqualizerArrow C K · f = limits.zero.ZeroArrow (equiv_Zero2 Z) (EqualizerObject C K) b.
  Proof.
    rewrite (EqualizerArrowEq C K). rewrite equiv_ZeroArrow.
    rewrite precomp_with_ZeroArrow. apply idpath.
  Qed.

  Lemma equiv_Kernel2_isEqualizer {a b : C} (f : C⟦a, b⟧) (K : Kernel f) :
    isKernel (equiv_Zero2 Z) (EqualizerArrow C K) f (equiv_Kernel2_eq f K).
  Proof.
    use (make_isKernel hs).
    intros w h H.
    use unique_exists.
    - use EqualizerIn.
      + exact h.
      + rewrite H.
        rewrite precomp_with_ZeroArrow.
        apply equiv_ZeroArrow.
    - use EqualizerArrowComm.
    - intros y. apply hs.
    - intros y T. cbn in T.
      use EqualizerInUnique. exact T.
  Qed.

  Definition equiv_Kernel2 {a b : C} (f : C⟦a, b⟧) (K : Kernel f) :
    limits.kernels.Kernel (equiv_Zero2 Z) f.
  Proof.
    use make_Kernel.
    - exact (EqualizerObject C K).
    - exact (EqualizerArrow C K).
    - exact (equiv_Kernel2_eq f K).
    - exact (equiv_Kernel2_isEqualizer f K).
  Defined.

End def_kernels.