Library UniMath.CategoryTheory.IdempotentsAndSplitting.Set

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.IdempotentsAndSplitting.Retracts.

Local Open Scope cat.

Section IdempotentsSplitInSet.

  Context {A : SET} {f : SET ⟦A , A ⟧} (p : f · f = f).

  Let I : UU := ∑ b : pr1 A , f b = b.
  Let J : SET.
  Show proof.

    exists I.
    apply isaset_total2.
    - apply A.
    - intro.
      apply isasetaprop.
      apply A.

Let pr : SET ⟦A , J ⟧.

Show proof.

    intro a.
    exists (f a).
    exact ((toforallpaths _ _ _ p) a).

  Let inc : SET ⟦J , A ⟧ := pr1.

  Lemma image_fact_gives_retraction
    : is_retraction inc pr.
  Show proof.

    apply funextsec.
    intro i.
    use subtypePath. {
      intro ; apply A.
    }
    exact (pr2 i).

Definition splitting_in_set : is_split_idempotent f.
Show proof.

    exists J.
    simple refine ((inc ,, pr ,, _) ,, _).
    - exact image_fact_gives_retraction.
    - apply funextsec ; intro ; apply idpath.

End IdempotentsSplitInSet.

Proposition idempotents_split_in_set
: idempotents_split SET.
Show proof.

  intro ; intro.
  apply hinhpr.
  apply splitting_in_set.
  apply f.